1 files changed, 15 insertions, 3 deletions
diff --git a/isar/Example.thy b/isar/Example.thy
index 22c0a4e1..179b5b83 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -11,15 +11,27 @@
 
 theory Example = Main:
 
+text {* Proper proof text. *}
+
 theorem and_comms: "A & B --> B & A"
 proof
   assume "A & B"
   thus "B & A"
   proof
-    assume A B
-    show ?thesis 
-      ..
+    assume B and A
+    thus ?thesis ..
   qed
 qed
 
+
+text {* Proof script. *}
+
+theorem "A & B --> B & A"
+  apply (rule impI)
+  apply (erule conjE)
+  apply (rule conjI)
+   apply assumption
+  apply assumption
+  done
+
 end