# HG changeset patch
# User haftmann
# Date 1242232895 -7200
# Node ID bfafc204042a25f94ab6798a306475d9d2341d8c
# Parent  94cb206f8f6a3d927e5b3f3ac94209d890c69c25
itself is instance of eq

diff -r 94cb206f8f6a -r bfafc204042a src/HOL/HOL.thy
--- 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]