src/HOL/Nat.thy
changeset 972 e61b058d58d2
parent 923 ff1574a81019
child 1151 c820b3cc3df0
     1.1 --- a/src/HOL/Nat.thy	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -59,9 +59,9 @@
     1.4    (*nat operations and recursion*)
     1.5    nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  \
     1.6  \                                        & (!x. n=Suc(x) --> z=f(x))"
     1.7 -  pred_nat_def  "pred_nat == {p. ? n. p = <n, Suc(n)>}"
     1.8 +  pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
     1.9  
    1.10 -  less_def "m<n == <m,n>:trancl(pred_nat)"
    1.11 +  less_def "m<n == (m,n):trancl(pred_nat)"
    1.12  
    1.13    le_def   "m<=(n::nat) == ~(n<m)"
    1.14