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