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