--- 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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Oct 28 00:07:51 2009 +0100
@@ -1,6 +1,9 @@
-(* Author: Lukas Bulwahn, TU Muenchen
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile.ML
+ Author: Lukas Bulwahn, TU Muenchen
+FIXME.
*)
+
signature PREDICATE_COMPILE =
sig
val setup : theory -> theory
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Oct 28 00:07:51 2009 +0100
@@ -1,8 +1,11 @@
-(* Author: Lukas Bulwahn, TU Muenchen
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
+ Author: Lukas Bulwahn, TU Muenchen
-Auxilary functions for predicate compiler
+Auxilary functions for predicate compiler.
*)
+(* FIXME proper signature *)
+
structure Predicate_Compile_Aux =
struct
@@ -234,6 +237,4 @@
intro'''''
end
-
-
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 28 00:07:51 2009 +0100
@@ -1,7 +1,7 @@
-(* Author: Lukas Bulwahn, TU Muenchen
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_core.ML
+ Author: Lukas Bulwahn, TU Muenchen
-(Prototype of) A compiler from predicates specified by intro/elim rules
-to equations.
+A compiler from predicates specified by intro/elim rules to equations.
*)
signature PREDICATE_COMPILE_CORE =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Oct 28 00:07:51 2009 +0100
@@ -1,8 +1,9 @@
-(* Author: Lukas Bulwahn, TU Muenchen
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_data.ML
+ Author: Lukas Bulwahn, TU Muenchen
-Book-keeping datastructure for the predicate compiler
+Book-keeping datastructure for the predicate compiler.
+*)
-*)
signature PREDICATE_COMPILE_DATA =
sig
type specification_table;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 28 00:07:51 2009 +0100
@@ -1,6 +1,7 @@
-(* Author: Lukas Bulwahn, TU Muenchen
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
+ Author: Lukas Bulwahn, TU Muenchen
-Preprocessing functions to predicates
+Preprocessing functions to predicates.
*)
signature PREDICATE_COMPILE_FUN =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Oct 28 00:07:51 2009 +0100
@@ -1,6 +1,7 @@
-(* Author: Lukas Bulwahn, TU Muenchen
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
+ Author: Lukas Bulwahn, TU Muenchen
-Preprocessing definitions of predicates to introduction rules
+Preprocessing definitions of predicates to introduction rules.
*)
signature PREDICATE_COMPILE_PRED =
@@ -16,7 +17,8 @@
(*val rewrite : thm -> thm*)
end;
-(* : PREDICATE_COMPILE_PREPROC_PRED *)
+
+(* : PREDICATE_COMPILE_PREPROC_PRED *) (* FIXME *)
structure Predicate_Compile_Pred =
struct
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Oct 28 00:07:51 2009 +0100
@@ -1,6 +1,7 @@
-(* Author: Lukas Bulwahn, TU Muenchen
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
+ Author: Lukas Bulwahn, TU Muenchen
-A quickcheck generator based on the predicate compiler
+A quickcheck generator based on the predicate compiler.
*)
signature PREDICATE_COMPILE_QUICKCHECK =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML Tue Oct 27 23:12:10 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML Wed Oct 28 00:07:51 2009 +0100
@@ -1,6 +1,7 @@
-(* Author: Lukas Bulwahn, TU Muenchen
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_set.ML
+ Author: Lukas Bulwahn, TU Muenchen
-Preprocessing sets to predicates
+Preprocessing sets to predicates.
*)
signature PREDICATE_COMPILE_SET =