src/HOL/Predicate_Compile.thy
changeset 33265 01c9c6dbd890
parent 33250 5c2af18a3237
child 34948 2d5f2a9f7601
--- a/src/HOL/Predicate_Compile.thy	Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Predicate_Compile.thy	Wed Oct 28 00:07:51 2009 +0100
@@ -1,4 +1,6 @@
-(* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *)
+(*  Title:      HOL/Predicate_Compile.thy
+    Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
+*)
 
 header {* A compiler for predicates defined by introduction rules *}
 
@@ -14,6 +16,6 @@
   "Tools/Predicate_Compile/predicate_compile.ML"
 begin
 
-setup {* Predicate_Compile.setup *}
+setup Predicate_Compile.setup
 
 end
\ No newline at end of file