src/HOL/List.thy
changeset 19363 667b5ea637dd
parent 19302 e1bda4fc1d1d
child 19390 6c7383f80ad1
     1.1 --- a/src/HOL/List.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/List.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -54,9 +54,9 @@
     1.4    filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
     1.5    map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list"
     1.6  
     1.7 -abbreviation (output)
     1.8 - upto:: "nat => nat => nat list"    ("(1[_../_])")
     1.9 -"[i..j] = [i..<(Suc j)]"
    1.10 +abbreviation
    1.11 +  upto:: "nat => nat => nat list"    ("(1[_../_])")
    1.12 +  "[i..j] == [i..<(Suc j)]"
    1.13  
    1.14  
    1.15  nonterminals lupdbinds lupdbind
    1.16 @@ -93,9 +93,9 @@
    1.17    Function @{text size} is overloaded for all datatypes. Users may
    1.18    refer to the list version as @{text length}. *}
    1.19  
    1.20 -abbreviation (output)
    1.21 - length :: "'a list => nat"
    1.22 -"length = size"
    1.23 +abbreviation
    1.24 +  length :: "'a list => nat"
    1.25 +  "length == size"
    1.26  
    1.27  primrec
    1.28    "hd(x#xs) = x"