# HG changeset patch
# User wenzelm
# Date 862922197 -7200
# Node ID 24ed05500380fe1ffcfe5681fb06281e20e61b23
# Parent  943f25285a3eac6078094cebf7e2d450ca54572a
tuned comments;

diff -r 943f25285a3e -r 24ed05500380 src/FOL/ex/Nat.ML
--- 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;
diff -r 943f25285a3e -r 24ed05500380 src/FOL/ex/Nat.thy
--- 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 +