src/HOL/List.thy
changeset 2262 c7ee913746fd
parent 1908 55d8e38262a8
child 2369 8100f00e8950
--- 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
-