# HG changeset patch
# User haftmann
# Date 1233004457 -3600
# Node ID 5111ce425e7a4fd3a3bcec0c9043ca02e6064d35
# Parent  d9294387ab0eef0022b5e124b9444a2e07009857
tuned header

diff -r d9294387ab0e -r 5111ce425e7a src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Mon Jan 26 22:14:16 2009 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Jan 26 22:14:17 2009 +0100
@@ -1,8 +1,5 @@
-(* 
-  ID:     $Id$
-  Author: Brian Huffman
-
-  Boolean algebras as locales.
+(*  Title:      HOL/Library/Boolean_Algebra.thy
+    Author:     Brian Huffman
 *)
 
 header {* Boolean Algebras *}
diff -r d9294387ab0e -r 5111ce425e7a src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Mon Jan 26 22:14:16 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Mon Jan 26 22:14:17 2009 +0100
@@ -1,11 +1,8 @@
-(*
-  ID:     $Id$
-  Author: Brian Huffman
-
-  Numeral Syntax for Types
+(*  Title:      HOL/Library/Numeral_Type.thy
+    Author:     Brian Huffman
 *)
 
-header "Numeral Syntax for Types"
+header {* Numeral Syntax for Types *}
 
 theory Numeral_Type
 imports Plain "~~/src/HOL/Presburger"
diff -r d9294387ab0e -r 5111ce425e7a src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Mon Jan 26 22:14:16 2009 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy	Mon Jan 26 22:14:17 2009 +0100
@@ -1,5 +1,4 @@
 (* 
-  ID:     $Id$
   Author: Gerwin Klein, NICTA
 
   Examples demonstrating and testing various word operations.
@@ -7,7 +6,8 @@
 
 header "Examples of word operations"
 
-theory WordExamples imports WordMain
+theory WordExamples
+imports Word
 begin
 
 -- "modulus"