From f582f005a4b337deef93995db1a918ea34a6c6d5 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Tue, 25 May 1999 12:19:10 +0000
Subject: more examples;

---
 isar/Example.thy | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index b8b7328b..8dc4b04a 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -1,12 +1,39 @@
 
 theory Example = Main:;
 
-lemma "A --> B --> A";
+
+lemma I: "A --> A";
+proof;
+  assume A;
+  show A; .;
+qed;
+
+lemma K: "A --> B --> A";
 proof;
   assume A;
   show "B --> A";
   proof;
+    show A; .;
   qed;
 qed;
 
+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

