author wenzelm Mon, 16 Feb 2009 20:23:43 +0100 changeset 29753 a9fc00f1b8f0 parent 29752 ad4e3a577fd3 child 29754 2203ef9b55ce
tuned;
 src/FOL/ex/Nat_Class.thy file | annotate | diff | comparison | revisions
```--- 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)```