--- 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 *}
--- 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"
--- 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"