# HG changeset patch
# User kleing
# Date 1187577875 -7200
# Node ID 22863f364531cf534a62e0d54b2e3942a80a3652
# Parent  e77ea0ea7f2c8bbc702f5938d9bcef1ace3c9bc4
added header

diff -r e77ea0ea7f2c -r 22863f364531 src/HOL/Word/BitSyntax.thy
--- a/src/HOL/Word/BitSyntax.thy	Mon Aug 20 04:34:31 2007 +0200
+++ b/src/HOL/Word/BitSyntax.thy	Mon Aug 20 04:44:35 2007 +0200
@@ -1,3 +1,11 @@
+(* 
+  ID:     $Id$
+  Author: Brian Huffman, PSU and Gerwin Klein, NICTA
+
+  Syntactic class for bitwise operations.
+*)
+
+
 header {* Syntactic class for bitwise operations *}
 
 theory BitSyntax
@@ -49,10 +57,10 @@
   "bit.B1 OR y = bit.B1"
   "bit.B0 XOR y = y"
   "bit.B1 XOR y = NOT y"
-by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def
-                  XOR_bit_def split: bit.split)
+  by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def
+                    XOR_bit_def split: bit.split)
 
 lemma bit_NOT_NOT: "NOT (NOT (b::bit)) = b"
-by (induct b) simp_all
+  by (induct b) simp_all
 
 end