src/FOL/ex/Nat_Class.thy
changeset 70047 01732226987a
parent 69602 e65314985426
     1.1 --- a/src/FOL/ex/Nat_Class.thy	Tue Mar 05 14:45:27 2019 +0100
     1.2 +++ b/src/FOL/ex/Nat_Class.thy	Tue Mar 05 16:40:12 2019 +0100
     1.3 @@ -2,17 +2,19 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  *)
     1.6  
     1.7 +section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
     1.8 +
     1.9  theory Nat_Class
    1.10 -imports FOL
    1.11 +  imports FOL
    1.12  begin
    1.13  
    1.14  text \<open>
    1.15 -  This is an abstract version of theory \<open>Nat\<close>. Instead of axiomatizing a
    1.16 -  single type \<open>nat\<close> we define the class of all these types (up to
    1.17 +  This is an abstract version of \<^file>\<open>Nat.thy\<close>. Instead of axiomatizing a
    1.18 +  single type \<open>nat\<close>, it defines the class of all these types (up to
    1.19    isomorphism).
    1.20  
    1.21 -  Note: The \<open>rec\<close> operator had to be made \<^emph>\<open>monomorphic\<close>, because class axioms
    1.22 -  may not contain more than one type variable.
    1.23 +  Note: The \<open>rec\<close> operator has been made \<^emph>\<open>monomorphic\<close>, because class
    1.24 +  axioms cannot contain more than one type variable.
    1.25  \<close>
    1.26  
    1.27  class nat =