# HG changeset patch # User lcp # Date 774023685 -7200 # Node ID 8bb25bc98a2741ff98006851da657b7cefa54c69 # Parent 8c9be2e9236dab272e66e32ec2360cdc4fde2d31 fixed indentation diff -r 8c9be2e9236d -r 8bb25bc98a27 Nat.thy --- a/Nat.thy Fri Jul 08 17:39:02 1994 +0200 +++ b/Nat.thy Tue Jul 12 16:34:45 1994 +0200 @@ -44,7 +44,7 @@ Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" (*nat operations and recursion*) nat_case_def "nat_case == (%n a f. @z. (n=0 --> z=a) \ -\ & (!x. n=Suc(x) --> z=f(x)))" +\ & (!x. n=Suc(x) --> z=f(x)))" pred_nat_def "pred_nat == {p. ? n. p = }" less_def "m:trancl(pred_nat)"