55 val Suml_name = "Datatype.Suml"; |
55 val Suml_name = "Datatype.Suml"; |
56 val Sumr_name = "Datatype.Sumr"; |
56 val Sumr_name = "Datatype.Sumr"; |
57 |
57 |
58 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, |
58 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, |
59 In0_eq, In1_eq, In0_not_In1, In1_not_In0, |
59 In0_eq, In1_eq, In0_not_In1, In1_not_In0, |
60 Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o Name) |
60 Lim_inject, Suml_inject, Sumr_inject] = |
|
61 map (fn a => get_thm Datatype_thy (Facts.Named (a, NONE))) |
61 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
62 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
62 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
63 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
63 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
64 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
64 |
65 |
65 val descr' = List.concat descr; |
66 val descr' = List.concat descr; |