author | blanchet |
Tue, 14 Sep 2010 13:24:18 +0200 | |
changeset 39359 | 6f49c7fbb1b1 |
parent 36046 | c3946372f556 |
child 40052 | ea46574ca815 |
permissions | -rw-r--r-- |
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 HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
4 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; 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 HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
6 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; 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 HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
9 |
uses |
5c2af18a3237
including the predicate compiler in HOL-Main; 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" |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
12 |
"Tools/Predicate_Compile/predicate_compile_core.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
13 |
"Tools/Predicate_Compile/predicate_compile_data.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
14 |
"Tools/Predicate_Compile/predicate_compile_fun.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
15 |
"Tools/Predicate_Compile/predicate_compile_pred.ML" |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36021
diff
changeset
|
16 |
"Tools/Predicate_Compile/predicate_compile_specialisation.ML" |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
17 |
"Tools/Predicate_Compile/predicate_compile.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
18 |
begin |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
19 |
|
33265 | 20 |
setup Predicate_Compile.setup |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
21 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33265
diff
changeset
|
22 |
end |