canonical approach towards lifting
authorhaftmann
Thu Feb 13 07:43:48 2020 +0100 (13 days ago)
changeset 71443ff6394cfc05c
parent 71442 d45495e897f4
child 71444 21c0b3a9d2f8
canonical approach towards lifting
src/HOL/ex/Bit_Lists.thy
src/HOL/ex/Word.thy
     1.1 --- a/src/HOL/ex/Bit_Lists.thy	Tue Feb 11 19:03:57 2020 +0100
     1.2 +++ b/src/HOL/ex/Bit_Lists.thy	Thu Feb 13 07:43:48 2020 +0100
     1.3 @@ -285,6 +285,8 @@
     1.4    "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"
     1.5    by (simp add: of_bits_int_def)
     1.6  
     1.7 +unbundle word.lifting
     1.8 +
     1.9  instantiation word :: (len) bit_representation
    1.10  begin
    1.11  
    1.12 @@ -303,6 +305,9 @@
    1.13  
    1.14  end
    1.15  
    1.16 +lifting_update word.lifting
    1.17 +lifting_forget word.lifting
    1.18 +
    1.19  
    1.20  subsection \<open>Bit representations with bit operations\<close>
    1.21  
     2.1 --- a/src/HOL/ex/Word.thy	Tue Feb 11 19:03:57 2020 +0100
     2.2 +++ b/src/HOL/ex/Word.thy	Thu Feb 13 07:43:48 2020 +0100
     2.3 @@ -715,4 +715,7 @@
     2.4  
     2.5  end
     2.6  
     2.7 +lifting_update word.lifting
     2.8 +lifting_forget word.lifting
     2.9 +
    2.10  end