don't generate code in Word because it breaks the current code setup
authorkuncar
Fri May 18 15:08:08 2012 +0200 (2012-05-18)
changeset 4794122e001795641
parent 47940 4ef90b51641e
child 47942 49b05b9ead33
don't generate code in Word because it breaks the current code setup
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Word/Word.thy	Thu May 17 13:36:23 2012 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Fri May 18 15:08:08 2012 +0200
     1.3 @@ -245,7 +245,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 Quotient_word reflp_word
     1.8 +setup_lifting(no_code) Quotient_word reflp_word
     1.9  
    1.10  text {* TODO: The next lemma could be generated automatically. *}
    1.11