equal
deleted
inserted
replaced
86 (* object implication to meta---*) |
86 (* object implication to meta---*) |
87 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
87 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
88 |
88 |
89 |
89 |
90 fun mir_tac ctxt q i = |
90 fun mir_tac ctxt q i = |
91 ObjectLogic.atomize_prems_tac i |
91 Object_Logic.atomize_prems_tac i |
92 THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i |
92 THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i |
93 THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i) |
93 THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i) |
94 THEN (fn st => |
94 THEN (fn st => |
95 let |
95 let |
96 val g = List.nth (prems_of st, i - 1) |
96 val g = List.nth (prems_of st, i - 1) |