author | kuncar |
Fri, 18 May 2012 15:08:08 +0200 | |
changeset 47941 | 22e001795641 |
parent 47940 | 4ef90b51641e |
child 47942 | 49b05b9ead33 |
--- a/src/HOL/Word/Word.thy Thu May 17 13:36:23 2012 +0200 +++ b/src/HOL/Word/Word.thy Fri May 18 15:08:08 2012 +0200 @@ -245,7 +245,7 @@ "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)" by (simp add: reflp_def) -setup_lifting Quotient_word reflp_word +setup_lifting(no_code) Quotient_word reflp_word text {* TODO: The next lemma could be generated automatically. *}