src/HOL/Word/Bits_Int.thy
changeset 58874 7172c7ffb047
parent 58410 6d46ad54a2ab
child 61799 4cf66f21b764
equal deleted inserted replaced
58873:db866dc081f8 58874:7172c7ffb047
     4   Definitions and basic theorems for bit-wise logical operations 
     4   Definitions and basic theorems for bit-wise logical operations 
     5   for integers expressed using Pls, Min, BIT,
     5   for integers expressed using Pls, Min, BIT,
     6   and converting them to and from lists of bools.
     6   and converting them to and from lists of bools.
     7 *) 
     7 *) 
     8 
     8 
     9 header {* Bitwise Operations on Binary Integers *}
     9 section {* Bitwise Operations on Binary Integers *}
    10 
    10 
    11 theory Bits_Int
    11 theory Bits_Int
    12 imports Bits Bit_Representation
    12 imports Bits Bit_Representation
    13 begin
    13 begin
    14 
    14