src/HOL/Predicate_Compile.thy
author bulwahn
Tue Oct 27 09:02:22 2009 +0100 (2009-10-27)
changeset 33250 5c2af18a3237
child 33265 01c9c6dbd890
permissions -rw-r--r--
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
     1 (* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *)
     2 
     3 header {* A compiler for predicates defined by introduction rules *}
     4 
     5 theory Predicate_Compile
     6 imports Quickcheck
     7 uses
     8   "Tools/Predicate_Compile/predicate_compile_aux.ML"
     9   "Tools/Predicate_Compile/predicate_compile_core.ML"
    10   "Tools/Predicate_Compile/predicate_compile_set.ML"
    11   "Tools/Predicate_Compile/predicate_compile_data.ML"
    12   "Tools/Predicate_Compile/predicate_compile_fun.ML"
    13   "Tools/Predicate_Compile/predicate_compile_pred.ML"
    14   "Tools/Predicate_Compile/predicate_compile.ML"
    15 begin
    16 
    17 setup {* Predicate_Compile.setup *}
    18 
    19 end