diff options
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 + + |