1.1 --- a/src/HOL/Word/BitSyntax.thy	Mon Aug 20 04:34:31 2007 +0200
     1.2 +++ b/src/HOL/Word/BitSyntax.thy	Mon Aug 20 04:44:35 2007 +0200
     1.3 @@ -1,3 +1,11 @@
     1.4 +(* 
     1.5 +  ID:     $Id$
     1.6 +  Author: Brian Huffman, PSU and Gerwin Klein, NICTA
     1.7 +
     1.8 +  Syntactic class for bitwise operations.
     1.9 +*)
    1.10 +
    1.11 +
    1.12  header {* Syntactic class for bitwise operations *}
    1.13  
    1.14  theory BitSyntax
    1.15 @@ -49,10 +57,10 @@
    1.16    "bit.B1 OR y = bit.B1"
    1.17    "bit.B0 XOR y = y"
    1.18    "bit.B1 XOR y = NOT y"
    1.19 -by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def
    1.20 -                  XOR_bit_def split: bit.split)
    1.21 +  by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def
    1.22 +                    XOR_bit_def split: bit.split)
    1.23  
    1.24  lemma bit_NOT_NOT: "NOT (NOT (b::bit)) = b"
    1.25 -by (induct b) simp_all
    1.26 +  by (induct b) simp_all
    1.27  
    1.28  end