# HG changeset patch
# User wenzelm
# Date 1142939890 -3600
# Node ID e1bda4fc1d1db361bab97e1e15c87eb2d1086f12
# Parent  ce99525202fcbb58491e294bc468b8b8ddb32b60
abbreviation upto, length;

diff -r ce99525202fc -r e1bda4fc1d1d src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Mar 21 12:18:09 2006 +0100
+++ b/src/HOL/List.thy	Tue Mar 21 12:18:10 2006 +0100
@@ -54,6 +54,10 @@
   filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list"
 
+abbreviation (output)
+ upto:: "nat => nat => nat list"    ("(1[_../_])")
+"[i..j] = [i..<(Suc j)]"
+
 
 nonterminals lupdbinds lupdbind
 
@@ -70,8 +74,6 @@
   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
   "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)
 
-  upto:: "nat => nat => nat list"    ("(1[_../_])")
-
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
@@ -80,8 +82,6 @@
   "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "list_update xs i x"
 
-  "[i..j]" == "[i..<(Suc j)]"
-
 
 syntax (xsymbols)
   "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
@@ -93,17 +93,9 @@
   Function @{text size} is overloaded for all datatypes. Users may
   refer to the list version as @{text length}. *}
 
-syntax length :: "'a list => nat"
-translations "length" => "size :: _ list => nat"
-
-typed_print_translation {*
-  let
-    fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] =
-          Syntax.const "length" $ t
-      | size_tr' _ _ _ = raise Match;
-  in [("size", size_tr')] end
-*}
-
+abbreviation (output)
+ length :: "'a list => nat"
+"length = size"
 
 primrec
   "hd(x#xs) = x"