tuned syntax
authoroheimb
Fri Jul 14 16:28:49 2000 +0200 (2000-07-14)
changeset 934140bab6613000
parent 9340 9666f78ecfab
child 9342 d66f25a206b4
tuned syntax
src/HOL/List.thy
src/HOL/Prod.thy
     1.1 --- a/src/HOL/List.thy	Fri Jul 14 16:27:45 2000 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Jul 14 16:28:49 2000 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    "@list"     :: args => 'a list                          ("[(_)]")
     1.5  
     1.6    (* Special syntax for filter *)
     1.7 -  "@filter"   :: [pttrn, 'a list, bool] => 'a list        ("(1[_:_ ./ _])")
     1.8 +  "@filter"   :: [pttrn, 'a list, bool] => 'a list        ("(1[_:_./ _])")
     1.9  
    1.10    (* list update *)
    1.11    "_lupdbind"      :: ['a, 'a] => lupdbind            ("(2_ :=/ _)")
     2.1 --- a/src/HOL/Prod.thy	Fri Jul 14 16:27:45 2000 +0200
     2.2 +++ b/src/HOL/Prod.thy	Fri Jul 14 16:28:49 2000 +0200
     2.3 @@ -49,10 +49,9 @@
     2.4  
     2.5  syntax
     2.6    "@Tuple"      :: "['a, args] => 'a * 'b"       ("(1'(_,/ _'))")
     2.7 -
     2.8 -  "_pattern"    :: [pttrn, patterns] => pttrn    ("'(_,/_')")
     2.9 -  ""            :: pttrn => patterns             ("_")
    2.10 -  "_patterns"   :: [pttrn, patterns] => patterns ("_,/_")
    2.11 +  "_pattern"    :: [pttrn, patterns] => pttrn      ("'(_,/ _')")
    2.12 +  ""            :: pttrn => patterns                     ("_")
    2.13 +  "_patterns"   :: [pttrn, patterns] => patterns     ("_,/ _")
    2.14  
    2.15    "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
    2.16    "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)