--- a/src/HOL/List.thy Mon Nov 27 13:44:56 1995 +0100
+++ b/src/HOL/List.thy Wed Nov 29 16:44:59 1995 +0100
@@ -13,28 +13,28 @@
consts
- "@" :: "['a list, 'a list] => 'a list" (infixr 65)
- drop :: "[nat, 'a list] => 'a list"
- filter :: "['a => bool, 'a list] => 'a list"
- flat :: "'a list list => 'a list"
- foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
- hd :: "'a list => 'a"
- length :: "'a list => nat"
- list_all :: "('a => bool) => ('a list => bool)"
- map :: "('a=>'b) => ('a list => 'b list)"
- mem :: "['a, 'a list] => bool" (infixl 55)
- nth :: "[nat, 'a list] => 'a"
- take :: "[nat, 'a list] => 'a list"
- tl,ttl :: "'a list => 'a list"
- rev :: "'a list => 'a list"
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ drop :: [nat, 'a list] => 'a list
+ filter :: ['a => bool, 'a list] => 'a list
+ flat :: 'a list list => 'a list
+ foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
+ hd :: 'a list => 'a
+ length :: 'a list => nat
+ list_all :: ('a => bool) => ('a list => bool)
+ map :: ('a=>'b) => ('a list => 'b list)
+ mem :: ['a, 'a list] => bool (infixl 55)
+ nth :: [nat, 'a list] => 'a
+ take :: [nat, 'a list] => 'a list
+ tl,ttl :: 'a list => 'a list
+ rev :: 'a list => 'a list
syntax
(* list Enumeration *)
- "@list" :: "args => 'a list" ("[(_)]")
+ "@list" :: args => 'a list ("[(_)]")
(* Special syntax for list_all and filter *)
- "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
- "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
+ "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
translations
"[x, xs]" == "x#[xs]"