# HG changeset patch
# User haftmann
# Date 1581576228 -3600
# Node ID ff6394cfc05c609605b68ef7c761d2b538c2e81b
# Parent  d45495e897f4c2040a93335c68fc4fad78e85ab6
canonical approach towards lifting

diff -r d45495e897f4 -r ff6394cfc05c src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Tue Feb 11 19:03:57 2020 +0100
+++ b/src/HOL/ex/Bit_Lists.thy	Thu Feb 13 07:43:48 2020 +0100
@@ -285,6 +285,8 @@
   "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"
   by (simp add: of_bits_int_def)
 
+unbundle word.lifting
+
 instantiation word :: (len) bit_representation
 begin
 
@@ -303,6 +305,9 @@
 
 end
 
+lifting_update word.lifting
+lifting_forget word.lifting
+
 
 subsection \<open>Bit representations with bit operations\<close>
 
diff -r d45495e897f4 -r ff6394cfc05c src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Tue Feb 11 19:03:57 2020 +0100
+++ b/src/HOL/ex/Word.thy	Thu Feb 13 07:43:48 2020 +0100
@@ -715,4 +715,7 @@
 
 end
 
+lifting_update word.lifting
+lifting_forget word.lifting
+
 end