aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2011-01-23 15:21:58 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2011-01-23 15:21:58 +0000
commit15fa4ae0b6c7527ea65bc2c0116fd1564f78df9c (patch)
tree9e6df46d4185036862b181bbf6ca614a244cacf0
parent3b4f52fee0d7798bf928d54d869c1e9750634ea4 (diff)
updated theory headers;
-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