--- a/src/HOL/List.thy Wed Nov 27 16:57:38 1996 +0100
+++ b/src/HOL/List.thy Wed Nov 27 17:00:25 1996 +0100
@@ -33,19 +33,26 @@
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]"
"[x]" == "x#[]"
-
"[x:xs . P]" == "filter (%x.P) xs"
"Alls x:xs.P" == "list_all (%x.P) xs"
+syntax (symbols)
+ "op #" :: ['a, 'a list] => 'a list (infixr "\\<bullet>" 65)
+ "op @" :: ['a list, 'a list] => 'a list (infixr "\\<circ>" 65)
+ "op mem" :: ['a, 'a list] => bool (infixl "\\<in>" 55)
+ "@Alls" :: [idt, 'a list, bool] => bool ("(2\\<forall> _\\<in>_./ _)" 10)
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
+
+
primrec hd list
"hd([]) = (@x.False)"
"hd(x#xs) = x"
@@ -95,4 +102,3 @@
defs
nth_def "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n"
end
-