(*
      Example proof document for Isabelle/Isar Proof General.
   
      Example-Xsym.thy,v 8.3 2005/09/17 11:10:30 makarius Exp
*)

theory "Example-Xsym" imports Main begin

text {* Proper proof text -- \textit{naive version}. *}

theorem and_comms: "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume "A \<and> B"
  then show "B \<and> A"
  proof
    assume B and A
    then
   show ?thesis ..
 qed
qed


text {* Proper proof text -- \textit{advanced version}. *}

theorem "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume "A \<and> B"
  then obtain B and A ..
  then show "B \<and> A" ..
qed


text {* Unstructured proof script. *}

theorem "A \<and> B \<longrightarrow> B \<and> A"
  apply (rule impI)
  apply (erule conjE)
  apply (rule conjI)
  apply assumption
  apply assumption
done

end