src/HOL/Word/Word.thy
changeset 59487 adaa430fc0f7
parent 59094 9ced35b4a2a9
child 59498 50b60f501b05
     1.1 --- a/src/HOL/Word/Word.thy	Fri Feb 06 19:17:17 2015 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Fri Feb 06 17:57:03 2015 +0100
     1.3 @@ -187,7 +187,7 @@
     1.4    "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
     1.5    by (simp add: reflp_def)
     1.6  
     1.7 -setup_lifting (no_code) Quotient_word reflp_word
     1.8 +setup_lifting Quotient_word reflp_word
     1.9  
    1.10  text {* TODO: The next lemma could be generated automatically. *}
    1.11