aboutsummaryrefslogtreecommitdiff
path: root/etc
diff options
context:
space:
mode:
Diffstat (limited to 'etc')
-rw-r--r--etc/isar/CommentParsingBug.thy2
-rw-r--r--etc/isar/CommentParsingBug2.thy2
2 files changed, 2 insertions, 2 deletions
diff --git a/etc/isar/CommentParsingBug.thy b/etc/isar/CommentParsingBug.thy
index 6a59a383..0da1575d 100644
--- a/etc/isar/CommentParsingBug.thy
+++ b/etc/isar/CommentParsingBug.thy
@@ -1,3 +1,3 @@
(**)(**)
-theory Scratch imports Main begin
+theory CommentParsingBug imports Main begin
diff --git a/etc/isar/CommentParsingBug2.thy b/etc/isar/CommentParsingBug2.thy
index 0c1a303e..a7bcba2b 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 imports Main begin
+theory CommentParsingBug2 imports Main begin
(*
defs