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