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