Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/AxClass/Nat/NatClass.thy
changeset 11099 b301d1f72552
parent 10140 ba9297b71897
child 16417 9bc16273c2d4 
--- a/doc-src/AxClass/Nat/NatClass.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/Nat/NatClass.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -19,7 +19,7 @@
   Suc :: "'a \<Rightarrow> 'a"
   rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
 
-axclass nat < "term"
+axclass nat \<subseteq> "term"
   induct: "P(\<zero>) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
   Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
   Suc_neq_0: "Suc(m) = \<zero> \<Longrightarrow> R"
isabelle