src/FOL/ex/Natural_Numbers.thy
changeset 12371 80ca9058db95
parent 11789 da81334357ba
child 14981 e73f8140af78
     1.1 --- a/src/FOL/ex/Natural_Numbers.thy	Wed Dec 05 03:05:39 2001 +0100
     1.2 +++ b/src/FOL/ex/Natural_Numbers.thy	Wed Dec 05 03:06:05 2001 +0100
     1.3 @@ -1,13 +1,18 @@
     1.4  (*  Title:      FOL/ex/Natural_Numbers.thy
     1.5      ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Munich
     1.7 -
     1.8 -Theory of the natural numbers: Peano's axioms, primitive recursion.
     1.9 -(Modernized version of Larry Paulson's theory "Nat".)
    1.10 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.11  *)
    1.12  
    1.13 +header {* Natural numbers *}
    1.14 +
    1.15  theory Natural_Numbers = FOL:
    1.16  
    1.17 +text {*
    1.18 +  Theory of the natural numbers: Peano's axioms, primitive recursion.
    1.19 +  (Modernized version of Larry Paulson's theory "Nat".)  \medskip
    1.20 +*}
    1.21 +
    1.22  typedecl nat
    1.23  arities nat :: "term"
    1.24