src/HOL/Predicate_Compile.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile.thy	Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,19 @@
+(* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *)
+
+header {* A compiler for predicates defined by introduction rules *}
+
+theory Predicate_Compile
+imports Quickcheck
+uses
+  "Tools/Predicate_Compile/predicate_compile_aux.ML"
+  "Tools/Predicate_Compile/predicate_compile_core.ML"
+  "Tools/Predicate_Compile/predicate_compile_set.ML"
+  "Tools/Predicate_Compile/predicate_compile_data.ML"
+  "Tools/Predicate_Compile/predicate_compile_fun.ML"
+  "Tools/Predicate_Compile/predicate_compile_pred.ML"
+  "Tools/Predicate_Compile/predicate_compile.ML"
+begin
+
+setup {* Predicate_Compile.setup *}
+
+end
\ No newline at end of file