equal
deleted
inserted
replaced
71 (* object implication to meta---*) |
71 (* object implication to meta---*) |
72 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
72 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
73 |
73 |
74 |
74 |
75 fun linr_tac ctxt q i = |
75 fun linr_tac ctxt q i = |
76 (ObjectLogic.atomize_tac i) |
76 (ObjectLogic.atomize_prems_tac i) |
77 THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)) |
77 THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)) |
78 THEN (fn st => |
78 THEN (fn st => |
79 let |
79 let |
80 val g = List.nth (prems_of st, i - 1) |
80 val g = List.nth (prems_of st, i - 1) |
81 val thy = ProofContext.theory_of ctxt |
81 val thy = ProofContext.theory_of ctxt |