blob: ff392ec39fde54cd3432802551b3df5be673a304 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
theory "Trac280-subrev" imports Main begin
lemma
assumes asm: "P\<^isub>i \<and> Q\<^isub>i"
shows "Q\<^isub>i \<and> P\<^isub>i"
proof -
from asm obtain "P\<^isub>i" and "Q\<^isub>i"
by blast
then show "Q\<^isub>i \<and> P\<^isub>i"
by simp
qed
end
|