equal
deleted
inserted
replaced
334 let |
334 let |
335 val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt; |
335 val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt; |
336 val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; |
336 val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; |
337 val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); |
337 val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); |
338 val tacs = Rs |> map (fn R => |
338 val tacs = Rs |> map (fn R => |
339 eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac); |
339 eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt); |
340 in fold_rev (curry op APPEND') tacs (K no_tac) i end); |
340 in fold_rev (curry op APPEND') tacs (K no_tac) i end); |
341 |
341 |
342 end; |
342 end; |
343 |
343 |
344 structure Basic_Goal: BASIC_GOAL = Goal; |
344 structure Basic_Goal: BASIC_GOAL = Goal; |