1 files changed, 6 insertions, 3 deletions
diff --git a/isar/Example.thy b/isar/Example.thy
index 720e5480..b0640146 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -9,10 +9,10 @@ theory Example imports Main begin
 
 text {* Proper proof text -- \textit{naive version}. *}
 
-theorem and_comms: "A & B --> B & A"
+theorem and_comms: "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
-  then show "B & A"
+  assume "A \<and> B"
+  then show "B \<and> A"
   proof
     assume B and A
     then show ?thesis ..
@@ -22,6 +22,9 @@ qed
 text {* Unstructured proof script. *}
 
 theorem  "A & B --> B & A"
+by and_comms
+
+
   apply (rule impI)
   apply (erule conjE)
   apply (rule conjI)