equal
deleted
inserted
replaced
144 map: "id :: 'a \<Rightarrow> 'a" |
144 map: "id :: 'a \<Rightarrow> 'a" |
145 bd: natLeq |
145 bd: natLeq |
146 rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" |
146 rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" |
147 by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) |
147 by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) |
148 |
148 |
149 definition id_bnf :: "'a \<Rightarrow> 'a" where "id_bnf \<equiv> (\<lambda>x. x)" |
149 definition id_bnf :: "'a \<Rightarrow> 'a" where |
|
150 "id_bnf \<equiv> (\<lambda>x. x)" |
150 |
151 |
151 lemma id_bnf_apply: "id_bnf x = x" |
152 lemma id_bnf_apply: "id_bnf x = x" |
152 unfolding id_bnf_def by simp |
153 unfolding id_bnf_def by simp |
153 |
154 |
154 bnf ID: 'a |
155 bnf ID: 'a |
175 DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer |
176 DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer |
176 ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id |
177 ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id |
177 ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep |
178 ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep |
178 ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer |
179 ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer |
179 |
180 |
180 hide_const (open) id_bnf |
|
181 hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV |
|
182 |
|
183 end |
181 end |