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