diff -r c3913a79b6ae -r 492493334e0f Nat.thy --- 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 = }" less_def "m:trancl(pred_nat)" le_def "m<=(n::nat) == ~(n