src/HOL/Arith.thy
changeset 4711 75a9ef36b1fe
parent 4360 40e5c97e988d
child 5183 89f162de39cf
     1.1 --- a/src/HOL/Arith.thy	Mon Mar 09 16:17:28 1998 +0100
     1.2 +++ b/src/HOL/Arith.thy	Mon Mar 09 16:30:55 1998 +0100
     1.3 @@ -22,9 +22,6 @@
     1.4    diff_0   "m - 0 = m"
     1.5    diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
     1.6  
     1.7 -syntax pred :: nat => nat
     1.8 -translations "pred m" => "m - 1"
     1.9 -
    1.10  primrec "op *"  nat 
    1.11    mult_0   "0 * n = 0"
    1.12    mult_Suc "Suc m * n = n + (m * n)"