aboutsummaryrefslogtreecommitdiff
path: root/etc/isar/CommentParsingBug2.thy
diff options
context:
space:
mode:
authorDavid Aspinall2009-08-17 16:27:25 +0000
committerDavid Aspinall2009-08-17 16:27:25 +0000
commite7c86841f0574ff2024c5fd54bf338a5af3ed3df (patch)
treeb686654d117d0483f00cd20c582d58800def1877 /etc/isar/CommentParsingBug2.thy
parent8465a954bceaaf378ec6bb61b2cf6f6738135bdd (diff)
Update some examples
Diffstat (limited to 'etc/isar/CommentParsingBug2.thy')
-rw-r--r--etc/isar/CommentParsingBug2.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/etc/isar/CommentParsingBug2.thy b/etc/isar/CommentParsingBug2.thy
index e92bd687..0c1a303e 100644
--- a/etc/isar/CommentParsingBug2.thy
+++ b/etc/isar/CommentParsingBug2.thy
@@ -1,5 +1,5 @@
(* Tobias reported 24.1.03. Could not repeat prob *)
-theory test = Main:
+theory test imports Main begin
(*
defs