Mercurial Mercurial > repos > Old_HOL / 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.
Nat.thy
changeset 249 492493334e0f
parent 185 8325414a370a 
--- a/Nat.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/Nat.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -57,14 +57,14 @@
   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
 
   (*nat operations and recursion*)
-  nat_case_def  "nat_case(a, f, n) == @z.  (n=0 --> z=a)  \
-\                                        & (!x. n=Suc(x) --> z=f(x))"
+  nat_case_def  "nat_case(a, f, n) == @z.  (n=0 --> z=a)  
+                                        & (!x. n=Suc(x) --> z=f(x))"
   pred_nat_def  "pred_nat == {p. ? n. p = <n, Suc(n)>}"
 
   less_def "m<n == <m,n>:trancl(pred_nat)"
 
   le_def   "m<=(n::nat) == ~(n<m)"
 
-  nat_rec_def   "nat_rec(n, c, d) == wfrec(pred_nat, n,   \
-\                        nat_case(%g.c, %m g. d(m, g(m))))"
+  nat_rec_def   "nat_rec(n, c, d) == wfrec(pred_nat, n,   
+                        nat_case(%g.c, %m g. d(m, g(m))))"
 end
Old_HOL