--- 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
--- 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