--- a/src/FOL/ex/Natural_Numbers.thy Wed Dec 05 03:05:39 2001 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy Wed Dec 05 03:06:05 2001 +0100
@@ -1,13 +1,18 @@
(* Title: FOL/ex/Natural_Numbers.thy
ID: $Id$
Author: Markus Wenzel, TU Munich
-
-Theory of the natural numbers: Peano's axioms, primitive recursion.
-(Modernized version of Larry Paulson's theory "Nat".)
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
+header {* Natural numbers *}
+
theory Natural_Numbers = FOL:
+text {*
+ Theory of the natural numbers: Peano's axioms, primitive recursion.
+ (Modernized version of Larry Paulson's theory "Nat".) \medskip
+*}
+
typedecl nat
arities nat :: "term"