tuned header
authorhaftmann
Mon Jan 26 22:14:17 2009 +0100 (2009-01-26)
changeset 296295111ce425e7a
parent 29628 d9294387ab0e
child 29630 199e2fb7f588
tuned header
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Word/Examples/WordExamples.thy
     1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Mon Jan 26 22:14:16 2009 +0100
     1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Jan 26 22:14:17 2009 +0100
     1.3 @@ -1,8 +1,5 @@
     1.4 -(* 
     1.5 -  ID:     $Id$
     1.6 -  Author: Brian Huffman
     1.7 -
     1.8 -  Boolean algebras as locales.
     1.9 +(*  Title:      HOL/Library/Boolean_Algebra.thy
    1.10 +    Author:     Brian Huffman
    1.11  *)
    1.12  
    1.13  header {* Boolean Algebras *}
     2.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Jan 26 22:14:16 2009 +0100
     2.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Jan 26 22:14:17 2009 +0100
     2.3 @@ -1,11 +1,8 @@
     2.4 -(*
     2.5 -  ID:     $Id$
     2.6 -  Author: Brian Huffman
     2.7 -
     2.8 -  Numeral Syntax for Types
     2.9 +(*  Title:      HOL/Library/Numeral_Type.thy
    2.10 +    Author:     Brian Huffman
    2.11  *)
    2.12  
    2.13 -header "Numeral Syntax for Types"
    2.14 +header {* Numeral Syntax for Types *}
    2.15  
    2.16  theory Numeral_Type
    2.17  imports Plain "~~/src/HOL/Presburger"
     3.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Mon Jan 26 22:14:16 2009 +0100
     3.2 +++ b/src/HOL/Word/Examples/WordExamples.thy	Mon Jan 26 22:14:17 2009 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (* 
     3.5 -  ID:     $Id$
     3.6    Author: Gerwin Klein, NICTA
     3.7  
     3.8    Examples demonstrating and testing various word operations.
     3.9 @@ -7,7 +6,8 @@
    3.10  
    3.11  header "Examples of word operations"
    3.12  
    3.13 -theory WordExamples imports WordMain
    3.14 +theory WordExamples
    3.15 +imports Word
    3.16  begin
    3.17  
    3.18  -- "modulus"