# HG changeset patch
# User paulson
# Date 933094720 -7200
# Node ID cfc11af6174a5c147b61fd8c953f3ac2e0799248
# Parent  6f18ae72a90e66140e9541e188b631a90e15b761
fixed the comments...

diff -r 6f18ae72a90e -r cfc11af6174a src/Sequents/LK/Nat.ML
--- a/src/Sequents/LK/Nat.ML	Tue Jul 27 18:52:48 1999 +0200
+++ b/src/Sequents/LK/Nat.ML	Tue Jul 27 18:58:40 1999 +0200
@@ -1,9 +1,9 @@
-(*  Title:      FOL/ex/Nat.ML
+(*  Title:      Sequents/LK/Nat
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
+    Copyright   1999  University of Cambridge
 
-Proofs about the natural numbers.
+Theory of the natural numbers: Peano's axioms, primitive recursion
 *)
 
 Addsimps [Suc_neq_0];
diff -r 6f18ae72a90e -r cfc11af6174a src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Tue Jul 27 18:52:48 1999 +0200
+++ b/src/Sequents/LK/Nat.thy	Tue Jul 27 18:58:40 1999 +0200
@@ -1,9 +1,7 @@
-(*  Title:      FOL/ex/Nat.thy
+(*  Title:      Sequents/LK/Nat
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Examples for the manuals.
+    Copyright   1999  University of Cambridge
 
 Theory of the natural numbers: Peano's axioms, primitive recursion
 *)
@@ -17,8 +15,9 @@
         "+" :: [nat, nat] => nat                (infixl 60)
 
 rules   
-  induct      "[| $H |- $E, P(0), $F;
-		  !!x. $H |- $E, P(x) --> P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
+  induct  "[| $H |- $E, P(0), $F;
+              !!x. $H |- $E, P(x) --> P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
+
   Suc_inject  "|- Suc(m)=Suc(n) --> m=n"
   Suc_neq_0   "|- Suc(m) ~= 0"
   rec_0       "|- rec(0,a,f) = a"