equal
deleted
inserted
replaced
51 |
51 |
52 end |
52 end |
53 |
53 |
54 |
54 |
55 nominal_datatype baz = |
55 nominal_datatype baz = |
56 Baz x::name t::foo bind x in t |
56 Baz x::name t::foo binds x in t |
57 |
57 |
58 |
58 |
59 |
59 |
60 thm baz.distinct |
60 thm baz.distinct |
61 thm baz.induct |
61 thm baz.induct |
76 |
76 |
77 nominal_datatype set_ty = |
77 nominal_datatype set_ty = |
78 Set_ty "nat set" |
78 Set_ty "nat set" |
79 | Fun "nat \<Rightarrow> nat" |
79 | Fun "nat \<Rightarrow> nat" |
80 | Var "name" |
80 | Var "name" |
81 | Lam x::"name" t::"set_ty" bind x in t |
81 | Lam x::"name" t::"set_ty" binds x in t |
82 thm meta_eq_to_obj_eq |
82 thm meta_eq_to_obj_eq |
83 thm set_ty.distinct |
83 thm set_ty.distinct |
84 thm set_ty.induct |
84 thm set_ty.induct |
85 thm set_ty.exhaust |
85 thm set_ty.exhaust |
86 thm set_ty.strong_exhaust |
86 thm set_ty.strong_exhaust |