# HG changeset patch
# User wenzelm
# Date 1551800412 -3600
# Node ID 01732226987a4b720101a53afd45f2bac7d39da2
# Parent  c28da0820b8b4ae3eed5d9b0ab1ef54282bb98a6
misc tuning and modernization;

diff -r c28da0820b8b -r 01732226987a src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Tue Mar 05 14:45:27 2019 +0100
+++ b/src/FOL/ex/Nat.thy	Tue Mar 05 16:40:12 2019 +0100
@@ -6,7 +6,7 @@
 section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
 
 theory Nat
-imports FOL
+  imports FOL
 begin
 
 typedecl nat
@@ -14,17 +14,17 @@
 
 axiomatization
   Zero :: \<open>nat\<close>  (\<open>0\<close>) and
-  Suc :: \<open>nat => nat\<close> and
-  rec :: \<open>[nat, 'a, [nat, 'a] => 'a] => 'a\<close>
+  Suc :: \<open>nat \<Rightarrow> nat\<close> and
+  rec :: \<open>[nat, 'a, [nat, 'a] \<Rightarrow> 'a] \<Rightarrow> 'a\<close>
 where
-  induct: \<open>[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)\<close> and
-  Suc_inject: \<open>Suc(m)=Suc(n) ==> m=n\<close> and
-  Suc_neq_0: \<open>Suc(m)=0 ==> R\<close> and
+  induct: \<open>\<lbrakk>P(0); \<And>x. P(x) \<Longrightarrow> P(Suc(x))\<rbrakk> \<Longrightarrow> P(n)\<close> and
+  Suc_inject: \<open>Suc(m)=Suc(n) \<Longrightarrow> m=n\<close> and
+  Suc_neq_0: \<open>Suc(m)=0 \<Longrightarrow> R\<close> and
   rec_0: \<open>rec(0,a,f) = a\<close> and
   rec_Suc: \<open>rec(Suc(m), a, f) = f(m, rec(m,a,f))\<close>
 
-definition add :: \<open>[nat, nat] => nat\<close>  (infixl \<open>+\<close> 60)
-  where \<open>m + n == rec(m, n, %x y. Suc(y))\<close>
+definition add :: \<open>[nat, nat] \<Rightarrow> nat\<close>  (infixl \<open>+\<close> 60)
+  where \<open>m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))\<close>
 
 
 subsection \<open>Proofs about the natural numbers\<close>
@@ -76,7 +76,7 @@
 done
 
 lemma
-  assumes prem: \<open>!!n. f(Suc(n)) = Suc(f(n))\<close>
+  assumes prem: \<open>\<And>n. f(Suc(n)) = Suc(f(n))\<close>
   shows \<open>f(i+j) = i+f(j)\<close>
 apply (rule_tac n = \<open>i\<close> in induct)
 apply simp
diff -r c28da0820b8b -r 01732226987a src/FOL/ex/Nat_Class.thy
--- a/src/FOL/ex/Nat_Class.thy	Tue Mar 05 14:45:27 2019 +0100
+++ b/src/FOL/ex/Nat_Class.thy	Tue Mar 05 16:40:12 2019 +0100
@@ -2,17 +2,19 @@
     Author:     Markus Wenzel, TU Muenchen
 *)
 
+section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
+
 theory Nat_Class
-imports FOL
+  imports FOL
 begin
 
 text \<open>
-  This is an abstract version of theory \<open>Nat\<close>. Instead of axiomatizing a
-  single type \<open>nat\<close> we define the class of all these types (up to
+  This is an abstract version of \<^file>\<open>Nat.thy\<close>. Instead of axiomatizing a
+  single type \<open>nat\<close>, it defines the class of all these types (up to
   isomorphism).
 
-  Note: The \<open>rec\<close> operator had to be made \<^emph>\<open>monomorphic\<close>, because class axioms
-  may not contain more than one type variable.
+  Note: The \<open>rec\<close> operator has been made \<^emph>\<open>monomorphic\<close>, because class
+  axioms cannot contain more than one type variable.
 \<close>
 
 class nat =