From 6189e10da761f1d63135efa068cc428454e069f2 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel <makarius@sketis.net>
Date: Fri, 24 Sep 1999 15:48:28 +0000
Subject: unified example with other proof assistants;

---
 isar/Example.thy | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'isar/Example.thy')

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;
 
-- 
cgit v1.2.3