equal
deleted
inserted
replaced
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 bind x in t |
57 |
57 |
58 |
58 |
|
59 |
59 thm baz.distinct |
60 thm baz.distinct |
60 thm baz.induct |
61 thm baz.induct |
61 thm baz.exhaust |
62 thm baz.exhaust |
62 thm baz.strong_exhaust |
63 thm baz.strong_exhaust |
63 thm baz.fv_defs |
64 thm baz.fv_defs |
76 nominal_datatype set_ty = |
77 nominal_datatype set_ty = |
77 Set_ty "nat set" |
78 Set_ty "nat set" |
78 | Fun "nat \<Rightarrow> nat" |
79 | Fun "nat \<Rightarrow> nat" |
79 | Var "name" |
80 | Var "name" |
80 | Lam x::"name" t::"set_ty" bind x in t |
81 | Lam x::"name" t::"set_ty" bind x in t |
81 |
82 thm meta_eq_to_obj_eq |
82 thm set_ty.distinct |
83 thm set_ty.distinct |
83 thm set_ty.induct |
84 thm set_ty.induct |
84 thm set_ty.exhaust |
85 thm set_ty.exhaust |
85 thm set_ty.strong_exhaust |
86 thm set_ty.strong_exhaust |
86 thm set_ty.fv_defs |
87 thm set_ty.fv_defs |