tuned headers;
authorwenzelm
Sun Mar 13 15:10:00 2011 +0100 (2011-03-13)
changeset 41941f823f7fae9a2
parent 41940 a3b68a7a0e15
child 41942 8d4881d895f8
tuned headers;
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/mode_inference.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Mar 13 14:51:38 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Mar 13 15:10:00 2011 +0100
     1.3 @@ -1,7 +1,8 @@
     1.4  (*  Title:      HOL/Tools/Predicate_Compile/code_prolog.ML
     1.5      Author:     Lukas Bulwahn, TU Muenchen
     1.6  
     1.7 -Prototype of an code generator for logic programming languages (a.k.a. Prolog)
     1.8 +Prototype of an code generator for logic programming languages
     1.9 +(a.k.a. Prolog).
    1.10  *)
    1.11  
    1.12  signature CODE_PROLOG =
     2.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Sun Mar 13 14:51:38 2011 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sun Mar 13 15:10:00 2011 +0100
     2.3 @@ -1,9 +1,9 @@
     2.4  (*  Title:      HOL/Tools/Predicate_Compile/core_data.ML
     2.5      Author:     Lukas Bulwahn, TU Muenchen
     2.6  
     2.7 -Data of the predicate compiler core
     2.8 +Data of the predicate compiler core.
     2.9 +*)
    2.10  
    2.11 -*)
    2.12  signature CORE_DATA =
    2.13  sig
    2.14    type mode = Predicate_Compile_Aux.mode
     3.1 --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Sun Mar 13 14:51:38 2011 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Sun Mar 13 15:10:00 2011 +0100
     3.3 @@ -1,8 +1,7 @@
     3.4  (*  Title:      HOL/Tools/Predicate_Compile/mode_inference.ML
     3.5      Author:     Lukas Bulwahn, TU Muenchen
     3.6  
     3.7 -Mode inference for the predicate compiler
     3.8 -
     3.9 +Mode inference for the predicate compiler.
    3.10  *)
    3.11  
    3.12  signature MODE_INFERENCE =
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Mar 13 14:51:38 2011 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Mar 13 15:10:00 2011 +0100
     4.3 @@ -1,7 +1,8 @@
     4.4  (*  Title:      HOL/Tools/Predicate_Compile/predicate_compile.ML
     4.5      Author:     Lukas Bulwahn, TU Muenchen
     4.6  
     4.7 -Entry point for the predicate compiler; definition of Toplevel commands code_pred and values
     4.8 +Entry point for the predicate compiler; definition of Toplevel
     4.9 +commands code_pred and values.
    4.10  *)
    4.11  
    4.12  signature PREDICATE_COMPILE =
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Sun Mar 13 14:51:38 2011 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Sun Mar 13 15:10:00 2011 +0100
     5.3 @@ -1,7 +1,7 @@
     5.4  (*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
     5.5      Author:     Lukas Bulwahn, TU Muenchen
     5.6  
     5.7 -Structures for different compilations of the predicate compiler
     5.8 +Structures for different compilations of the predicate compiler.
     5.9  *)
    5.10  
    5.11  structure PredicateCompFuns =