equal
deleted
inserted
replaced
1 (* Author: Lukas Bulwahn, TU Muenchen |
1 (* Title: HOL/Tools/Predicate_Compile/predicate_compile_pred.ML |
|
2 Author: Lukas Bulwahn, TU Muenchen |
2 |
3 |
3 Preprocessing definitions of predicates to introduction rules |
4 Preprocessing definitions of predicates to introduction rules. |
4 *) |
5 *) |
5 |
6 |
6 signature PREDICATE_COMPILE_PRED = |
7 signature PREDICATE_COMPILE_PRED = |
7 sig |
8 sig |
8 (* preprocesses an equation to a set of intro rules; defines new constants *) |
9 (* preprocesses an equation to a set of intro rules; defines new constants *) |
14 val preprocess_term : term -> theory -> (term list * theory) |
15 val preprocess_term : term -> theory -> (term list * theory) |
15 |
16 |
16 (*val rewrite : thm -> thm*) |
17 (*val rewrite : thm -> thm*) |
17 |
18 |
18 end; |
19 end; |
19 (* : PREDICATE_COMPILE_PREPROC_PRED *) |
20 |
|
21 (* : PREDICATE_COMPILE_PREPROC_PRED *) (* FIXME *) |
20 structure Predicate_Compile_Pred = |
22 structure Predicate_Compile_Pred = |
21 struct |
23 struct |
22 |
24 |
23 open Predicate_Compile_Aux |
25 open Predicate_Compile_Aux |
24 |
26 |