equal
deleted
inserted
replaced
64 |
64 |
65 (* object implication to meta---*) |
65 (* object implication to meta---*) |
66 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
66 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
67 |
67 |
68 |
68 |
69 fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st => |
69 fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st => |
70 let |
70 let |
71 val g = List.nth (prems_of st, i - 1) |
71 val g = List.nth (prems_of st, i - 1) |
72 val thy = ProofContext.theory_of ctxt |
72 val thy = ProofContext.theory_of ctxt |
73 (* Transform the term*) |
73 (* Transform the term*) |
74 val (t,np,nh) = prepare_for_linz q g |
74 val (t,np,nh) = prepare_for_linz q g |