equal
deleted
inserted
replaced
228 "the_In1r" == "the_Inr \<circ> the_In1" |
228 "the_In1r" == "the_Inr \<circ> the_In1" |
229 |
229 |
230 ML {* |
230 ML {* |
231 fun sum3_instantiate ctxt thm = map (fn s => |
231 fun sum3_instantiate ctxt thm = map (fn s => |
232 simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}]) |
232 simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}]) |
233 (RuleInsts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] |
233 (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] |
234 *} |
234 *} |
235 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
235 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
236 |
236 |
237 translations |
237 translations |
238 "option"<= (type) "Datatype.option" |
238 "option"<= (type) "Datatype.option" |