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
bulwahn@33250
     1
(* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *)
bulwahn@33250
     2
bulwahn@33250
     3
header {* A compiler for predicates defined by introduction rules *}
bulwahn@33250
     4
bulwahn@33250
     5
theory Predicate_Compile
bulwahn@33250
     6
imports Quickcheck
bulwahn@33250
     7
uses
bulwahn@33250
     8
  "Tools/Predicate_Compile/predicate_compile_aux.ML"
bulwahn@33250
     9
  "Tools/Predicate_Compile/predicate_compile_core.ML"
bulwahn@33250
    10
  "Tools/Predicate_Compile/predicate_compile_set.ML"
bulwahn@33250
    11
  "Tools/Predicate_Compile/predicate_compile_data.ML"
bulwahn@33250
    12
  "Tools/Predicate_Compile/predicate_compile_fun.ML"
bulwahn@33250
    13
  "Tools/Predicate_Compile/predicate_compile_pred.ML"
bulwahn@33250
    14
  "Tools/Predicate_Compile/predicate_compile.ML"
bulwahn@33250
    15
begin
bulwahn@33250
    16
bulwahn@33250
    17
setup {* Predicate_Compile.setup *}
bulwahn@33250
    18
bulwahn@33250
    19
end