| changeset 47566 | c201a1fe0a81 |
| parent 47521 | 69f95ac85c3d |
| child 47567 | 407cabf66f21 |
--- a/src/HOL/Word/Word.thy Wed Apr 18 23:13:11 2012 +0200 +++ b/src/HOL/Word/Word.thy Wed Apr 18 23:57:44 2012 +0200 @@ -243,9 +243,7 @@ "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)" by (simp add: reflp_def) -local_setup {* - Lifting_Setup.setup_by_quotient @{thm Quotient_word} (SOME @{thm reflp_word}) -*} +setup_lifting Quotient_word reflp_word text {* TODO: The next lemma could be generated automatically. *}