src/CTT/Arith.thy
changeset 1474 3f7d67927fe2
parent 0 a5a9c433f639
child 3837 d7f033c74b38
     1.1 --- a/src/CTT/Arith.thy	Mon Feb 05 13:44:28 1996 +0100
     1.2 +++ b/src/CTT/Arith.thy	Mon Feb 05 14:44:09 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	CTT/arith
     1.5 +(*  Title:      CTT/arith
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1991  University of Cambridge
    1.10  
    1.11  Arithmetic operators and their definitions
    1.12 @@ -11,8 +11,8 @@
    1.13  
    1.14  Arith = CTT +
    1.15  
    1.16 -consts "#+","-","|-|"	:: "[i,i]=>i"	(infixr 65)
    1.17 -       "#*",div,mod     :: "[i,i]=>i"	(infixr 70)
    1.18 +consts "#+","-","|-|"   :: "[i,i]=>i"   (infixr 65)
    1.19 +       "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
    1.20  
    1.21  rules
    1.22    add_def     "a#+b == rec(a, b, %u v.succ(v))"