equal
deleted
inserted
replaced
291 "atomic" indicates if the goal should be wrapped up in the function |
291 "atomic" indicates if the goal should be wrapped up in the function |
292 "Goal::prop=>prop" to avoid assumptions being returned separately. |
292 "Goal::prop=>prop" to avoid assumptions being returned separately. |
293 *) |
293 *) |
294 fun prepare_proof atomic rths chorn = |
294 fun prepare_proof atomic rths chorn = |
295 let |
295 let |
296 val _ = legacy_feature "Old goal command"; |
|
297 val thy = Thm.theory_of_cterm chorn; |
296 val thy = Thm.theory_of_cterm chorn; |
298 val horn = Thm.term_of chorn; |
297 val horn = Thm.term_of chorn; |
299 val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; |
298 val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; |
300 val (As, B) = Logic.strip_horn horn; |
299 val (As, B) = Logic.strip_horn horn; |
301 val atoms = atomic andalso |
300 val atoms = atomic andalso |
512 val Goal = Goalw []; |
511 val Goal = Goalw []; |
513 |
512 |
514 (*simple version with minimal amount of checking and postprocessing*) |
513 (*simple version with minimal amount of checking and postprocessing*) |
515 fun simple_prove_goal_cterm G f = |
514 fun simple_prove_goal_cterm G f = |
516 let |
515 let |
517 val _ = legacy_feature "Old goal command"; |
|
518 val As = Drule.strip_imp_prems G; |
516 val As = Drule.strip_imp_prems G; |
519 val B = Drule.strip_imp_concl G; |
517 val B = Drule.strip_imp_concl G; |
520 val asms = map Assumption.assume As; |
518 val asms = map Assumption.assume As; |
521 fun check NONE = error "prove_goal: tactic failed" |
519 fun check NONE = error "prove_goal: tactic failed" |
522 | check (SOME (thm, _)) = (case nprems_of thm of |
520 | check (SOME (thm, _)) = (case nprems_of thm of |