src/HOL/HOL.thy
changeset 31956 c3844c4d0c2c
parent 31902 862ae16a799d
child 31998 2c7a24f74db9
     1.1 --- a/src/HOL/HOL.thy	Tue Jul 07 07:56:24 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jul 07 17:21:26 2009 +0200
     1.3 @@ -1869,7 +1869,27 @@
     1.4  declare simp_thms(6) [code nbe]
     1.5  
     1.6  setup {*
     1.7 -  Code.add_const_alias @{thm equals_eq}
     1.8 +  Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
     1.9 +*}
    1.10 +
    1.11 +lemma equals_alias_cert: "OFCLASS('a, eq_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> eq)" (is "?ofclass \<equiv> ?eq")
    1.12 +proof
    1.13 +  assume "PROP ?ofclass"
    1.14 +  show "PROP ?eq"
    1.15 +    by (tactic {* ALLGOALS (rtac (Drule.unconstrainTs @{thm equals_eq})) *}) 
    1.16 +      (fact `PROP ?ofclass`)
    1.17 +next
    1.18 +  assume "PROP ?eq"
    1.19 +  show "PROP ?ofclass" proof
    1.20 +  qed (simp add: `PROP ?eq`)
    1.21 +qed
    1.22 +  
    1.23 +setup {*
    1.24 +  Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>eq \<Rightarrow> 'a \<Rightarrow> bool"})
    1.25 +*}
    1.26 +
    1.27 +setup {*
    1.28 +  Code.add_const_alias @{thm equals_alias_cert}
    1.29  *}
    1.30  
    1.31  hide (open) const eq