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