equal
deleted
inserted
replaced
31 sig |
31 sig |
32 |
32 |
33 exception eqsubst_occL_exp of |
33 exception eqsubst_occL_exp of |
34 string * (int list) * (thm list) * int * thm; |
34 string * (int list) * (thm list) * int * thm; |
35 |
35 |
36 |
36 type match |
37 type match = |
37 type searchinfo |
38 ((indexname * (sort * typ)) list (* type instantiations *) |
|
39 * (indexname * (typ * term)) list) (* term instantiations *) |
|
40 * (string * typ) list (* fake named type abs env *) |
|
41 * (string * typ) list (* type abs env *) |
|
42 * term (* outer term *) |
|
43 |
|
44 type searchinfo = |
|
45 theory (* sign for matching *) |
|
46 * int (* maxidx *) |
|
47 * BasicIsaFTerm.FcTerm (* focusterm to search under *) |
|
48 |
38 |
49 val prep_subst_in_asm : |
39 val prep_subst_in_asm : |
50 int (* subgoal to subst in *) |
40 int (* subgoal to subst in *) |
51 -> thm (* target theorem with subgoals *) |
41 -> thm (* target theorem with subgoals *) |
52 -> int (* premise to subst in *) |
42 -> int (* premise to subst in *) |