--- 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"