src/HOL/Mirabelle/Mirabelle_Test.thy
changeset 32564 378528d2f7eb
parent 32518 e3c4e337196c
child 38892 eccc9e2a6412
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Sat Sep 12 16:30:48 2009 +0200
@@ -1,5 +1,5 @@
-(* Title: Mirabelle_Test.thy
-   Author: Sascha Boehme
+(*  Title:      HOL/Mirabelle/Mirabelle_Test.thy
+    Author:     Sascha Boehme, TU Munich
 *)
 
 header {* Simple test theory for Mirabelle actions *}
@@ -14,9 +14,9 @@
   "Tools/mirabelle_sledgehammer.ML"
 begin
 
-(*
-  only perform type-checking of the actions,
-  any reasonable test would be too complicated
-*)
+text {*
+  Only perform type-checking of the actions,
+  any reasonable test would be too complicated.
+*}
 
 end