| changeset 35898 | c890a3835d15 |
| parent 35890 | 14a0993fe64b |
| child 36021 | c86fcf44b4c9 |
| 35897:8758895ea413 | 35898:c890a3835d15 |
|---|---|
1 |
|
2 (* Title: HOL/Predicate_Compile.thy |
1 (* Title: HOL/Predicate_Compile.thy |
3 Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen |
2 Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* A compiler for predicates defined by introduction rules *} |
5 header {* A compiler for predicates defined by introduction rules *} |