summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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 =