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