unified example with other proof assistants;

1 files changed, 10 insertions, 4 deletions

diff --git a/isar/Example.thy b/isar/Example.thy
index c213de4d..2b9c72f6 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -1,13 +1,19 @@
+(*
+    Example proof document for Isabelle/Isar Proof General.
+ 
+    $Id$
+*)
+
 
 theory Example = Main:;
 
-lemma and_comms: "A & B --> B & A";
+theorem and_comms: "A & B --> B & A";
 proof;
   assume "A & B";
-  show "B & A";
+  thus "B & A";
   proof;
-    from prems; show B; ..;
-    from prems; show A; ..;
+    assume B A;
+    thus ?thesis; ..;
   qed;
 qed;