src/HOL/List.thy
changeset 3507 157be29ad5ba
parent 3465 e85c24717cad
child 3584 8f9ee0f79d9a
     1.1 --- a/src/HOL/List.thy	Mon Jul 07 10:49:14 1997 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Jul 09 12:57:04 1997 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  (*Function "size" is overloaded for all datatypes.  Users may refer to the
     1.5    list version as "length".*)
     1.6  syntax   length :: 'a list => nat
     1.7 -translations  "length"  =>  "size"
     1.8 +translations  "length"  =>  "size:: _ list => nat"
     1.9  
    1.10  primrec hd list
    1.11    "hd([]) = arbitrary"
    1.12 @@ -111,3 +111,19 @@
    1.13    "dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)"
    1.14  
    1.15  end
    1.16 +
    1.17 +ML
    1.18 +
    1.19 +local
    1.20 +
    1.21 +(* translating size::list -> length *)
    1.22 +
    1.23 +fun size_tr' (Type ("fun", (Type ("list", _) :: _))) [t] =
    1.24 +      Syntax.const "length" $ t
    1.25 +  | size_tr'   _ _ = raise Match;
    1.26 +
    1.27 +in
    1.28 +
    1.29 +val typed_print_translation = [("size", size_tr')];
    1.30 +
    1.31 +end;