# 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 = <n, Suc(n)>}"
 
   less_def "m<n == <m,n>:trancl(pred_nat)"