# HG changeset patch
# User wenzelm
# Date 1256684912 -3600
# Node ID 2172ae12c81d23babc66e3e38cf334c73cd6d97c
# Parent  a0f5896d877e325b5c8eeaa8690e2a0651e1e23a# Parent  01c9c6dbd890827ef88e4450517004eb30033925
merged

diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Predicate_Compile.thy	Wed Oct 28 00:08:32 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
diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Oct 28 00:08:32 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
diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Oct 28 00:08:32 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;
diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 28 00:08:32 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 =
diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Oct 28 00:08:32 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;
diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Oct 28 00:08:32 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 =
diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Oct 28 00:08:32 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
 
diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Oct 28 00:08:32 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 =
diff -r a0f5896d877e -r 2172ae12c81d src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML	Tue Oct 27 23:16:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML	Wed Oct 28 00:08:32 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 =