equal
deleted
inserted
replaced
1 (* Title: HOL/Predicate_Compile.thy |
1 (* Title: HOL/Predicate_Compile.thy |
2 Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen |
2 Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 header {* A compiler for predicates defined by introduction rules *} |
5 section {* A compiler for predicates defined by introduction rules *} |
6 |
6 |
7 theory Predicate_Compile |
7 theory Predicate_Compile |
8 imports Random_Sequence Quickcheck_Exhaustive |
8 imports Random_Sequence Quickcheck_Exhaustive |
9 keywords "code_pred" :: thy_goal and "values" :: diag |
9 keywords "code_pred" :: thy_goal and "values" :: diag |
10 begin |
10 begin |