equal
deleted
inserted
replaced
173 rl); |
173 rl); |
174 |
174 |
175 (*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
175 (*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
176 val meta_outer = |
176 val meta_outer = |
177 curry_rule o standard o |
177 curry_rule o standard o |
178 rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI] |
178 rule_by_tactic (REPEAT |
179 ORELSE' etac conjE)); |
179 (FIRSTGOAL (resolve_tac [allI, impI, conjI] |
|
180 ORELSE' etac conjE))); |
180 |
181 |
181 (*Strip off the outer !P*) |
182 (*Strip off the outer !P*) |
182 val spec'= read_instantiate [("x","P::?'b=>bool")] spec; |
183 val spec'= read_instantiate [("x","P::?'b=>bool")] spec; |
183 |
184 |
184 val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; |
185 val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; |