From 59075f938201d52e82437938d4d71e06e7e6555d Mon Sep 17 00:00:00 2001
From: Makarius Wenzel <makarius@sketis.net>
Date: Tue, 21 Sep 1999 09:49:11 +0000
Subject: lemma and_comms;

---
 isar/Example.thy | 44 +++++---------------------------------------
 1 file changed, 5 insertions(+), 39 deletions(-)

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 84d56e14..c213de4d 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -1,48 +1,14 @@
 
 theory Example = Main:;
 
-text {*
- Just a few tiny examples to get an idea of how Isabelle/Isar proof documents
- may look like.
- *};
-
-lemma I: "A --> A";
-proof;
-  assume A;
-  show A; .;
-qed;
-
-lemma K: "A --> B --> A";
+lemma and_comms: "A & B --> B & A";
 proof;
-  assume A;
-  show "B --> A";
+  assume "A & B";
+  show "B & A";
   proof;
-    show A; .;
+    from prems; show B; ..;
+    from prems; show A; ..;
   qed;
 qed;
 
-text {*
- This one is a good test for Proof General to cope with block-structured
- proof texts.  Have fun with automatic indentation!
- *};
-
-lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
-proof;
-  assume "A --> B --> C";
-  show "(A --> B) --> A --> C";
-  proof;
-    assume "A --> B";
-    show "A --> C";
-    proof;
-      assume A;
-      show C;
-      proof (rule mp);
-	show "B --> C"; by (rule mp);
-        show B; by (rule mp);
-      qed;
-    qed;
-  qed;
-qed;
-
-
 end;
-- 
cgit v1.2.3