lemma and_comms;

1 files changed, 5 insertions, 39 deletions

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;