diff -r e8d4606e6502 -r 3f7d67927fe2 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CTT/Arith.thy	Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	CTT/arith
+(*  Title:      CTT/arith
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
 Arithmetic operators and their definitions
@@ -11,8 +11,8 @@
 
 Arith = CTT +
 
-consts "#+","-","|-|"	:: "[i,i]=>i"	(infixr 65)
-       "#*",div,mod     :: "[i,i]=>i"	(infixr 70)
+consts "#+","-","|-|"   :: "[i,i]=>i"   (infixr 65)
+       "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
 
 rules
   add_def     "a#+b == rec(a, b, %u v.succ(v))"