equal
deleted
inserted
replaced
48 |
48 |
49 in |
49 in |
50 |
50 |
51 fun deriv_tac ctxt = SUBGOAL (fn (prem, i) => |
51 fun deriv_tac ctxt = SUBGOAL (fn (prem, i) => |
52 resolve_tac @{thms deriv_rulesI} i ORELSE |
52 resolve_tac @{thms deriv_rulesI} i ORELSE |
53 ((rtac (RuleInsts.read_instantiate ctxt [(("f", 0), get_fun_name prem)] |
53 ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)] |
54 @{thm DERIV_chain2}) i) handle DERIV_name => no_tac)); |
54 @{thm DERIV_chain2}) i) handle DERIV_name => no_tac)); |
55 |
55 |
56 fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i)); |
56 fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i)); |
57 |
57 |
58 end |
58 end |