src/FOL/ex/Nat.thy

--- a/src/FOL/ex/Nat.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Nat.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -29,7 +29,7 @@
 
 subsection \<open>Proofs about the natural numbers\<close>
 
-lemma Suc_n_not_n: "Suc(k) ~= k"
+lemma Suc_n_not_n: "Suc(k) \<noteq> k"
 apply (rule_tac n = k in induct)
 apply (rule notI)
 apply (erule Suc_neq_0)