# HG changeset patch
# User wenzelm
# Date 849110425 -3600
# Node ID c7ee913746fdea781e3c892e16a2ead53b9a68f7
# Parent  d926157c0a6a503c30aa79648b022f38494d3381
added symbols syntax;

diff -r d926157c0a6a -r c7ee913746fd src/HOL/List.thy
--- 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
-