equal
deleted
inserted
replaced
245 In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3" |
245 In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3" |
246 translations |
246 translations |
247 "In1l e" == "In1 (Inl e)" |
247 "In1l e" == "In1 (Inl e)" |
248 "In1r c" == "In1 (Inr c)" |
248 "In1r c" == "In1 (Inr c)" |
249 |
249 |
|
250 syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al" |
|
251 the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar" |
|
252 translations |
|
253 "the_In1l" == "the_Inl \<circ> the_In1" |
|
254 "the_In1r" == "the_Inr \<circ> the_In1" |
|
255 |
250 ML {* |
256 ML {* |
251 fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq]) |
257 fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq]) |
252 (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] |
258 (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] |
253 *} |
259 *} |
254 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
260 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |