src/HOL/Arith.thy
changeset 3308 da002cef7090
parent 3235 351565b7321b
child 3366 2402c6ab1561
     1.1 --- a/src/HOL/Arith.thy	Thu May 22 18:29:17 1997 +0200
     1.2 +++ b/src/HOL/Arith.thy	Fri May 23 09:17:26 1997 +0200
     1.3 @@ -14,6 +14,8 @@
     1.4  consts
     1.5    pred      :: nat => nat
     1.6    div, mod  :: [nat, nat] => nat  (infixl 70)
     1.7 +  (* size of a datatype value; overloaded *)
     1.8 +  size      :: 'a => nat
     1.9  
    1.10  defs
    1.11    pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"