--- a/src/FOL/ex/Nat.ML Tue May 06 13:49:29 1997 +0200
+++ b/src/FOL/ex/Nat.ML Tue May 06 14:36:37 1997 +0200
@@ -1,13 +1,9 @@
-(* Title: FOL/ex/nat.ML
+(* Title: FOL/ex/Nat.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Examples for the manual "Introduction to Isabelle"
-
-Proofs about the natural numbers
-
-INCOMPATIBLE with nat2.ML, Nipkow's examples
+Proofs about the natural numbers.
To generate similar output to manual, execute these commands:
Pretty.setmargin 72; print_depth 0;
--- a/src/FOL/ex/Nat.thy Tue May 06 13:49:29 1997 +0200
+++ b/src/FOL/ex/Nat.thy Tue May 06 14:36:37 1997 +0200
@@ -1,13 +1,11 @@
-(* Title: FOL/ex/nat.thy
+(* Title: FOL/ex/Nat.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Examples for the manual "Introduction to Isabelle"
+Examples for the manuals.
Theory of the natural numbers: Peano's axioms, primitive recursion
-
-INCOMPATIBLE with nat2.thy, Nipkow's example
*)
Nat = FOL +