author | wenzelm |
Sat, 13 Mar 2010 14:44:47 +0100 | |
changeset 35743 | c506c029a082 |
parent 34948 | 2d5f2a9f7601 |
child 35879 | 99818df5b8f5 |
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 |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33265
diff
changeset
|
8 |
imports Random_Sequence Quickcheck |
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" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
11 |
"Tools/Predicate_Compile/predicate_compile_core.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
12 |
"Tools/Predicate_Compile/predicate_compile_set.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" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
16 |
"Tools/Predicate_Compile/predicate_compile.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
17 |
begin |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
18 |
|
33265 | 19 |
setup Predicate_Compile.setup |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
20 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33265
diff
changeset
|
21 |
end |