etc/isar/Trac280-subrev.thy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

theory Test 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