src/HOL/HOL.thy
changeset 61076 bdc1e2f0a86a
parent 60781 2da59cdf531c
child 61144 5e94dfead1c2
     1.1 --- a/src/HOL/HOL.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -1792,7 +1792,7 @@
     1.4    "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
     1.5    by (simp add: equal)
     1.6  
     1.7 -setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
     1.8 +setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
     1.9  
    1.10  lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
    1.11  proof
    1.12 @@ -1806,7 +1806,7 @@
    1.13    qed (simp add: \<open>PROP ?equal\<close>)
    1.14  qed
    1.15  
    1.16 -setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
    1.17 +setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::equal \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
    1.18  
    1.19  setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close>
    1.20