equal
deleted
inserted
replaced
152 end |
152 end |
153 |
153 |
154 bnf DEADID: 'a |
154 bnf DEADID: 'a |
155 map: "id :: 'a \<Rightarrow> 'a" |
155 map: "id :: 'a \<Rightarrow> 'a" |
156 bd: natLeq |
156 bd: natLeq |
157 rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" |
157 rel: "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" |
158 by (auto simp add: natLeq_card_order natLeq_cinfinite) |
158 by (auto simp add: natLeq_card_order natLeq_cinfinite) |
159 |
159 |
160 definition id_bnf :: "'a \<Rightarrow> 'a" where |
160 definition id_bnf :: "'a \<Rightarrow> 'a" where |
161 "id_bnf \<equiv> (\<lambda>x. x)" |
161 "id_bnf \<equiv> (\<lambda>x. x)" |
162 |
162 |