equal
deleted
inserted
replaced
1 (* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *) |
1 (* Title: HOL/Predicate_Compile.thy |
|
2 Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen |
|
3 *) |
2 |
4 |
3 header {* A compiler for predicates defined by introduction rules *} |
5 header {* A compiler for predicates defined by introduction rules *} |
4 |
6 |
5 theory Predicate_Compile |
7 theory Predicate_Compile |
6 imports Quickcheck |
8 imports Quickcheck |
12 "Tools/Predicate_Compile/predicate_compile_fun.ML" |
14 "Tools/Predicate_Compile/predicate_compile_fun.ML" |
13 "Tools/Predicate_Compile/predicate_compile_pred.ML" |
15 "Tools/Predicate_Compile/predicate_compile_pred.ML" |
14 "Tools/Predicate_Compile/predicate_compile.ML" |
16 "Tools/Predicate_Compile/predicate_compile.ML" |
15 begin |
17 begin |
16 |
18 |
17 setup {* Predicate_Compile.setup *} |
19 setup Predicate_Compile.setup |
18 |
20 |
19 end |
21 end |