From a8c139b902656d2269882cc2497dbb58bfdf10e8 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 3 Aug 2010 13:34:56 +0000
Subject: Fix theory name

---
 etc/isar/MultipleModes.thy | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'etc/isar')

diff --git a/etc/isar/MultipleModes.thy b/etc/isar/MultipleModes.thy
index af36ed51..7e552570 100644
--- a/etc/isar/MultipleModes.thy
+++ b/etc/isar/MultipleModes.thy
@@ -1,6 +1,6 @@
 header {* Some tests for \textbf{multiple modes!!} *}
 
-theory Example = Main:
+theory MultipleModes imports Main begin
 
 text {* Proper proof text -- \textit{naive version}. *}
 
@@ -15,10 +15,13 @@ proof
  qed
 qed
 
-ML_setup {*
+ML {*
   fun fact 0 = 1 
     | fact n = n * (fact (n-1))
 
   val x = 7; 
 *}
 
+end
+
+
-- 
cgit v1.2.3