changeset 67399 | eab6ce8368fa |
parent 67091 | 1393c2340eec |
child 67613 | ce654b0e6d69 |
--- a/src/HOL/BNF_Composition.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/BNF_Composition.thy Wed Jan 10 15:25:09 2018 +0100 @@ -154,7 +154,7 @@ bnf DEADID: 'a map: "id :: 'a \<Rightarrow> 'a" bd: natLeq - rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" + rel: "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" by (auto simp add: natLeq_card_order natLeq_cinfinite) definition id_bnf :: "'a \<Rightarrow> 'a" where