equal
deleted
inserted
replaced
252 fun add_conv ctxt ctrm = |
252 fun add_conv ctxt ctrm = |
253 (case Thm.term_of ctrm of |
253 (case Thm.term_of ctrm of |
254 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
254 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
255 (Conv.binop_conv (add_conv ctxt) |
255 (Conv.binop_conv (add_conv ctxt) |
256 then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm |
256 then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm |
257 | _ $ _ => Conv.combination_conv |
257 | _ $ _ => Conv.comb_conv (add_conv ctxt) ctrm |
258 (add_conv ctxt) (add_conv ctxt) ctrm |
|
259 | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm |
258 | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm |
260 | _ => Conv.all_conv ctrm) |
259 | _ => Conv.all_conv ctrm) |
261 |
260 |
262 fun add_tac ctxt = CSUBGOAL (fn (goal, i) => |
261 fun add_tac ctxt = CSUBGOAL (fn (goal, i) => |
263 CONVERSION |
262 CONVERSION |