canonical approach towards lifting
authorhaftmann
Thu, 13 Feb 2020 07:43:48 +0100
changeset 71655 ff6394cfc05c
parent 71654 d45495e897f4
child 71656 21c0b3a9d2f8
canonical approach towards lifting
src/HOL/ex/Bit_Lists.thy
src/HOL/ex/Word.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>
 
--- 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