1 files changed, 24 insertions, 0 deletions
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; 
+*}
+