1.1 --- a/src/HOL/HOL.thy	Tue May 12 21:39:19 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed May 13 18:41:35 2009 +0200
     1.3 @@ -1836,6 +1836,22 @@
     1.4  
     1.5  lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
     1.6  
     1.7 +instantiation itself :: (type) eq
     1.8 +begin
     1.9 +
    1.10 +definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
    1.11 +  "eq_itself x y \<longleftrightarrow> x = y"
    1.12 +
    1.13 +instance proof
    1.14 +qed (fact eq_itself_def)
    1.15 +
    1.16 +end
    1.17 +
    1.18 +lemma eq_itself_code [code]:
    1.19 +  "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
    1.20 +  by (simp add: eq)
    1.21 +
    1.22 +
    1.23  text {* Equality *}
    1.24  
    1.25  declare simp_thms(6) [code nbe]