equal
deleted
inserted
replaced
1 (* Author: Lukas Bulwahn, TU Muenchen |
1 (* Title: HOL/Tools/Predicate_Compile/predicate_compile_core.ML |
2 |
2 Author: Lukas Bulwahn, TU Muenchen |
3 (Prototype of) A compiler from predicates specified by intro/elim rules |
3 |
4 to equations. |
4 A compiler from predicates specified by intro/elim rules to equations. |
5 *) |
5 *) |
6 |
6 |
7 signature PREDICATE_COMPILE_CORE = |
7 signature PREDICATE_COMPILE_CORE = |
8 sig |
8 sig |
9 val setup: theory -> theory |
9 val setup: theory -> theory |