# HG changeset patch
# User huffman
# Date 1131664177 -3600
# Node ID 0c05abaf6244814ccbb0d22f575fd5badfab0511
# Parent  a084aa91f70175f5f6463761052c6fc4ec7e1f8f
add header

diff -r a084aa91f701 -r 0c05abaf6244 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Nov 10 21:14:05 2005 +0100
+++ b/src/HOL/Divides.thy	Fri Nov 11 00:09:37 2005 +0100
@@ -2,9 +2,9 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
+*)
 
-The division operators div, mod and the divides relation "dvd"
-*)
+header {* The division operators div, mod and the divides relation "dvd" *}
 
 theory Divides
 imports Datatype
diff -r a084aa91f701 -r 0c05abaf6244 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Nov 10 21:14:05 2005 +0100
+++ b/src/HOL/Fun.thy	Fri Nov 11 00:09:37 2005 +0100
@@ -2,9 +2,9 @@
     ID:         $Id$
     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
+*)
 
-Notions about functions.
-*)
+header {* Notions about functions *}
 
 theory Fun
 imports Typedef