46 rec_thms : thm list, |
46 rec_thms : thm list, |
47 case_thms : thm list list, |
47 case_thms : thm list list, |
48 split_thms : (thm * thm) list, |
48 split_thms : (thm * thm) list, |
49 induction : thm, |
49 induction : thm, |
50 simps : thm list} * theory |
50 simps : thm list} * theory |
51 val rep_datatype : string list option -> (thmref * Attrib.src list) list list -> |
51 val rep_datatype : string list option -> (Facts.ref * Attrib.src list) list list -> |
52 (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory -> |
52 (Facts.ref * Attrib.src list) list list -> Facts.ref * Attrib.src list -> theory -> |
53 {distinct : thm list list, |
53 {distinct : thm list list, |
54 inject : thm list list, |
54 inject : thm list list, |
55 exhaustion : thm list, |
55 exhaustion : thm list, |
56 rec_thms : thm list, |
56 rec_thms : thm list, |
57 case_thms : thm list list, |
57 case_thms : thm list list, |
389 (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1, |
389 (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1, |
390 atac 2, resolve_tac thms 1, etac FalseE 1])) |
390 atac 2, resolve_tac thms 1, etac FalseE 1])) |
391 | ManyConstrs (thm, simpset) => |
391 | ManyConstrs (thm, simpset) => |
392 let |
392 let |
393 val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] = |
393 val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] = |
394 map (get_thm (ThyInfo.the_theory "Datatype" thy) o Name) |
394 map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE))) |
395 ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]; |
395 ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]; |
396 in |
396 in |
397 Goal.prove (Simplifier.the_context ss) [] [] eq_t (K |
397 Goal.prove (Simplifier.the_context ss) [] [] eq_t (K |
398 (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1, |
398 (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1, |
399 full_simp_tac (Simplifier.inherit_context ss simpset) 1, |
399 full_simp_tac (Simplifier.inherit_context ss simpset) 1, |