equal
deleted
inserted
replaced
1 (* Author: Lukas Bulwahn, TU Muenchen |
1 (* Title: HOL/Tools/Predicate_Compile/predicate_compile_fun.ML |
2 |
2 Author: Lukas Bulwahn, TU Muenchen |
3 Preprocessing functions to predicates |
3 |
|
4 Preprocessing functions to predicates. |
4 *) |
5 *) |
5 |
6 |
6 signature PREDICATE_COMPILE_FUN = |
7 signature PREDICATE_COMPILE_FUN = |
7 sig |
8 sig |
8 val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory |
9 val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory |