From 06c81062dc8bb7fbbf058cb3a9eed5b100e4bc76 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 14 Dec 2007 13:17:29 +0000
Subject: New files.

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

(limited to 'etc')

diff --git a/etc/isar/MMMtests.thy b/etc/isar/MMMtests.thy
new file mode 100644
index 00000000..76f84993
--- /dev/null
+++ b/etc/isar/MMMtests.thy
@@ -0,0 +1,40 @@
+(* Testing samples for MMM *)
+
+header {* This is edited in LaTeX mode *}
+
+theory MMMtests imports Main begin
+
+text {*
+  This is a test of MMM support.
+  This region is edited in \LaTeX{} mode.
+*}
+
+subsection {* and this one. *}
+
+
+ML_setup {*
+  (* Whereas this region is edited in SML mode.  For that to work, you
+  need to have installed SML mode in your Emacs, otherwise MMM mode
+  won't bother.  See Stefan Monnier's page at
+  http://www.iro.umontreal.ca/~monnier/elisp/. *)
+  
+  fun foo [] = 0
+    | foo (x::xs) = x * foo xs
+*}
+
+ML {* (* and this one *) *}
+
+ML_command {* (* and this one *) *}
+
+typed_print_translation {* (* and even this one *) *}
+
+text {* 
+  You can enter the text for a MMM region conveniently 
+  using the dedicated insertion commands. For example, I inserted
+  this region by typing \texttt{C-c \% t}  --- see the MMM menu or
+  \texttt{C-c \% h}  for a list of commands.  
+
+  Notice that font locking for different modes tends to interact
+  badly with mode switches between lines.  Best stick to
+  separate lines as in these examples.
+*}
-- 
cgit v1.2.3