src/HOL/Arith.thy
changeset 5183 89f162de39cf
parent 4711 75a9ef36b1fe
child 8929 4829556a56f8
     1.1 --- a/src/HOL/Arith.thy	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/Arith.thy	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -14,15 +14,15 @@
     1.4  (* size of a datatype value; overloaded *)
     1.5  consts size :: 'a => nat
     1.6  
     1.7 -primrec "op +" nat 
     1.8 +primrec
     1.9    add_0    "0 + n = n"
    1.10    add_Suc  "Suc m + n = Suc(m + n)"
    1.11  
    1.12 -primrec "op -" nat 
    1.13 +primrec
    1.14    diff_0   "m - 0 = m"
    1.15    diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    1.16  
    1.17 -primrec "op *"  nat 
    1.18 +primrec
    1.19    mult_0   "0 * n = 0"
    1.20    mult_Suc "Suc m * n = n + (m * n)"
    1.21