equal
deleted
inserted
replaced
66 (*Terms containing a case statement must be post-processed with the |
66 (*Terms containing a case statement must be post-processed with the |
67 ML function transform_case. There, all asterikses before the "=" |
67 ML function transform_case. There, all asterikses before the "=" |
68 will be replaced by the expression between the two asterisks |
68 will be replaced by the expression between the two asterisks |
69 following "case" and the asterisk after esac will be deleted *) |
69 following "case" and the asterisk after esac will be deleted *) |
70 |
70 |
71 oracle mc_mucke_oracle ("term") = |
71 oracle mc_mucke_oracle = mk_mc_mucke_oracle |
72 mk_mc_mucke_oracle |
|
73 |
72 |
74 ML {* |
73 ML {* |
75 (* search_mu t searches for Mu terms in term t. In the case of nested Mu's, |
74 (* search_mu t searches for Mu terms in term t. In the case of nested Mu's, |
76 it yields innermost one. If no Mu term is present, search_mu yields NONE |
75 it yields innermost one. If no Mu term is present, search_mu yields NONE |
77 *) |
76 *) |
152 end |
151 end |
153 end; |
152 end; |
154 end; |
153 end; |
155 |
154 |
156 |
155 |
157 fun call_mucke_tac i state = |
156 val call_mucke_tac = CSUBGOAL (fn (cgoal, i) => |
158 let val thy = Thm.theory_of_thm state; |
157 let val OraAss = mc_mucke_oracle cgoal |
159 val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state)) |
158 in cut_facts_tac [OraAss] i end); |
160 in |
|
161 (cut_facts_tac [OraAss] i) state |
|
162 end; |
|
163 |
159 |
164 |
160 |
165 (* transforming fun-defs into lambda-defs *) |
161 (* transforming fun-defs into lambda-defs *) |
166 |
162 |
167 val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g"; |
163 val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g"; |