author  bulwahn 
Thu, 21 Oct 2010 19:13:09 +0200  
changeset 40052  ea46574ca815 
parent 36046  c3946372f556 
child 45450  dc2236b19a3d 
permissions  rwrr 
33265  1 
(* Title: HOL/Predicate_Compile.thy 
2 
Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen 

3 
*) 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

4 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

5 
header {* A compiler for predicates defined by introduction rules *} 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

6 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

7 
theory Predicate_Compile 
36021  8 
imports New_Random_Sequence 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

9 
uses 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

10 
"Tools/Predicate_Compile/predicate_compile_aux.ML" 
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
36032
diff
changeset

11 
"Tools/Predicate_Compile/predicate_compile_compilations.ML" 
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
36046
diff
changeset

12 
"Tools/Predicate_Compile/core_data.ML" 
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
36046
diff
changeset

13 
"Tools/Predicate_Compile/mode_inference.ML" 
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
36046
diff
changeset

14 
"Tools/Predicate_Compile/predicate_compile_proof.ML" 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

15 
"Tools/Predicate_Compile/predicate_compile_core.ML" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

16 
"Tools/Predicate_Compile/predicate_compile_data.ML" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

17 
"Tools/Predicate_Compile/predicate_compile_fun.ML" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

18 
"Tools/Predicate_Compile/predicate_compile_pred.ML" 
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36021
diff
changeset

19 
"Tools/Predicate_Compile/predicate_compile_specialisation.ML" 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

20 
"Tools/Predicate_Compile/predicate_compile.ML" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

21 
begin 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

22 

33265  23 
setup Predicate_Compile.setup 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

24 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33265
diff
changeset

25 
end 