# HG changeset patch
# User wenzelm
# Date 1234812223 -3600
# Node ID a9fc00f1b8f0d08a8bbdac277dc737bbc6747c51
# Parent  ad4e3a577fd30a0418dba9e4942318ce926cf960
tuned;

diff -r ad4e3a577fd3 -r a9fc00f1b8f0 src/FOL/ex/Nat_Class.thy
--- a/src/FOL/ex/Nat_Class.thy	Mon Feb 16 20:15:40 2009 +0100
+++ b/src/FOL/ex/Nat_Class.thy	Mon Feb 16 20:23:43 2009 +0100
@@ -7,7 +7,7 @@
 begin
 
 text {*
-  This is an abstract version of theory @{text "Nat"}. Instead of
+  This is an abstract version of theory @{text Nat}. Instead of
   axiomatizing a single type @{text nat} we define the class of all
   these types (up to isomorphism).
 
@@ -17,7 +17,7 @@
 
 class nat =
   fixes Zero :: 'a  ("0")
-    and Suc :: "'a => 'a"
+    and Suc :: "'a \<Rightarrow> 'a"
     and rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
   assumes induct: "P(0) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
     and Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
@@ -30,7 +30,7 @@
   add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 60) where
   "m + n = rec(m, n, \<lambda>x y. Suc(y))"
 
-lemma Suc_n_not_n: "Suc(k) ~= (k::'a)"
+lemma Suc_n_not_n: "Suc(k) \<noteq> (k::'a)"
   apply (rule_tac n = k in induct)
    apply (rule notI)
    apply (erule Suc_neq_Zero)