equal
deleted
inserted
replaced
252 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
252 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
253 get_sum_thm ctxt trm (dest_sum trm) |
253 get_sum_thm ctxt trm (dest_sum trm) |
254 | _ => Conv.all_conv ctrm |
254 | _ => Conv.all_conv ctrm |
255 end |
255 end |
256 |
256 |
257 val add_conv = More_Conv.bottom_conv add_simple_conv |
257 val add_conv = Conv.bottom_conv add_simple_conv |
258 |
258 |
259 fun add_tac ctxt = CONVERSION (add_conv ctxt)*} |
259 fun add_tac ctxt = CONVERSION (add_conv ctxt)*} |
260 |
260 |
261 text {* |
261 text {* |
262 A test case for this conversion is as follows |
262 A test case for this conversion is as follows |