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 ++++++++++++++++++++++++
 etc/mmm-install            | 17 +++++++++++++++++
 2 files changed, 41 insertions(+)
 create mode 100644 etc/isar/MultipleModes.thy
 create mode 100644 etc/mmm-install

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; 
+*}
+
diff --git a/etc/mmm-install b/etc/mmm-install
new file mode 100644
index 00000000..41042d23
--- /dev/null
+++ b/etc/mmm-install
@@ -0,0 +1,17 @@
+#!/bin/sh
+#
+# Install from mmm-mode into PG by copying relevant files
+# Run from inside mmm-mode distrib
+#
+# $Id$
+#
+NOTICES="AUTHORS COPYING FAQ INSTALL NEWS README TODO"
+DOCS="mmm.texinfo version.texi"
+ELISP=*.el
+MMMDIR=~/PG/mmm
+
+rm -f $MMMDIR/*
+cp -p $NOTICES $DOCS $ELISP $MMMDIR
+
+
+
-- 
cgit v1.2.3