--- a/src/HOL/List.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/List.thy Mon Feb 05 21:27:16 1996 +0100
@@ -13,7 +13,7 @@
consts
- "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ "@" :: ['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
@@ -22,7 +22,7 @@
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)
+ mem :: ['a, 'a list] => bool (infixl 55)
nth :: [nat, 'a list] => 'a
take :: [nat, 'a list] => 'a list
tl,ttl :: 'a list => 'a list
@@ -33,15 +33,15 @@
"@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]"
"[x]" == "x#[]"
- "[x:xs . P]" == "filter (%x.P) xs"
- "Alls x:xs.P" == "list_all (%x.P) xs"
+ "[x:xs . P]" == "filter (%x.P) xs"
+ "Alls x:xs.P" == "list_all (%x.P) xs"
primrec hd list
hd_Nil "hd([]) = (@x.False)"