src/HOL/Predicate_Compile.thy
changeset 33250 5c2af18a3237
child 33265 01c9c6dbd890
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Predicate_Compile.thy	Tue Oct 27 09:02:22 2009 +0100
     1.3 @@ -0,0 +1,19 @@
     1.4 +(* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header {* A compiler for predicates defined by introduction rules *}
     1.7 +
     1.8 +theory Predicate_Compile
     1.9 +imports Quickcheck
    1.10 +uses
    1.11 +  "Tools/Predicate_Compile/predicate_compile_aux.ML"
    1.12 +  "Tools/Predicate_Compile/predicate_compile_core.ML"
    1.13 +  "Tools/Predicate_Compile/predicate_compile_set.ML"
    1.14 +  "Tools/Predicate_Compile/predicate_compile_data.ML"
    1.15 +  "Tools/Predicate_Compile/predicate_compile_fun.ML"
    1.16 +  "Tools/Predicate_Compile/predicate_compile_pred.ML"
    1.17 +  "Tools/Predicate_Compile/predicate_compile.ML"
    1.18 +begin
    1.19 +
    1.20 +setup {* Predicate_Compile.setup *}
    1.21 +
    1.22 +end
    1.23 \ No newline at end of file