diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-03 13:34:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-03 13:34:56 +0000 |
| commit | a8c139b902656d2269882cc2497dbb58bfdf10e8 (patch) | |
| tree | 9ee00644d5d5b2aba4c4712b2bdd18c758b7ebe8 /etc/isar | |
| parent | 94bb3e91c134e09e194be2f8778ff5def909674d (diff) | |
Fix theory name
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/MultipleModes.thy | 7 |
1 files changed, 5 insertions, 2 deletions
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 + + |