From 63c2385e812fbe3c32071e2c2a01270f09b38e3b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 18 Feb 2003 01:04:15 +0000
Subject: New files.

---
 etc/isar/MultipleModes.thy | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 etc/isar/MultipleModes.thy

(limited to 'etc/isar/MultipleModes.thy')

diff --git a/etc/isar/MultipleModes.thy b/etc/isar/MultipleModes.thy
new file mode 100644
index 00000000..af36ed51
--- /dev/null
+++ b/etc/isar/MultipleModes.thy
@@ -0,0 +1,24 @@
+header {* Some tests for \textbf{multiple modes!!} *}
+
+theory Example = Main:
+
+text {* Proper proof text -- \textit{naive version}. *}
+
+theorem and_comms: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then
+   show ?thesis ..
+ qed
+qed
+
+ML_setup {*
+  fun fact 0 = 1 
+    | fact n = n * (fact (n-1))
+
+  val x = 7; 
+*}
+
-- 
cgit v1.2.3