--- a/src/HOL/HOL.thy Tue May 12 21:39:19 2009 +0200
+++ b/src/HOL/HOL.thy Wed May 13 18:41:35 2009 +0200
@@ -1836,6 +1836,22 @@
lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
+instantiation itself :: (type) eq
+begin
+
+definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
+ "eq_itself x y \<longleftrightarrow> x = y"
+
+instance proof
+qed (fact eq_itself_def)
+
+end
+
+lemma eq_itself_code [code]:
+ "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
+ by (simp add: eq)
+
+
text {* Equality *}
declare simp_thms(6) [code nbe]