tuned pattern syntax;
authorwenzelm
Mon Sep 22 17:31:57 1997 +0200 (1997-09-22)
changeset 36929f9bcce140ce
parent 3691 f0396ac63e12
child 3693 37aa547fb564
tuned pattern syntax;
src/HOL/Modelcheck/MCSyn.thy
src/HOL/Prod.thy
src/HOL/W0/Maybe.thy
src/ZF/ZF.thy
     1.1 --- a/src/HOL/Modelcheck/MCSyn.thy	Mon Sep 22 17:31:28 1997 +0200
     1.2 +++ b/src/HOL/Modelcheck/MCSyn.thy	Mon Sep 22 17:31:57 1997 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Modelcheck/MCSyn.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Olaf M"uller, Jan Philipps, Robert Sandner
     1.7 +    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     1.8      Copyright   1997  TU Muenchen
     1.9  *)
    1.10  
    1.11 @@ -19,10 +19,10 @@
    1.12    "? "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
    1.13    "ALL " 	:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
    1.14    "EX "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
    1.15 -   "_lambda"	:: [idts, 'a::logic] => 'b::logic	("(3L _./ _)" 10)
    1.16 +   "_lambda"	:: [pttrns, 'a] => 'b			("(3L _./ _)" 10)
    1.17  
    1.18 -  "_idts"     	:: [pttrn, idts] => idts		("_,/_" [1, 0] 0)
    1.19 -  "_pttrn"      :: [pttrn, pttrns] => pttrn     	("_,/_" [1, 0] 0)
    1.20 +  "_idts"     	:: [idt, idts] => idts		        ("_,/_" [1, 0] 0)
    1.21 +  "_pattern"    :: [pttrn, patterns] => pttrn     	("_,/_" [1, 0] 0)
    1.22  
    1.23    "Mu "		:: [idts, 'a pred] => 'a pred		("(3[mu _./ _])" 1000)
    1.24    "Nu "		:: [idts, 'a pred] => 'a pred		("(3[nu _./ _])" 1000)
     2.1 --- a/src/HOL/Prod.thy	Mon Sep 22 17:31:28 1997 +0200
     2.2 +++ b/src/HOL/Prod.thy	Mon Sep 22 17:31:57 1997 +0200
     2.3 @@ -39,16 +39,16 @@
     2.4  
     2.5  (* patterns -- extends pre-defined type "pttrn" used in abstractions *)
     2.6  
     2.7 -types pttrns
     2.8 +types patterns
     2.9  
    2.10  syntax
    2.11 -  "@Tuple"      :: "['a, args] => 'a * 'b"      ("(1'(_,/ _'))")
    2.12 +  "@Tuple"      :: "['a, args] => 'a * 'b"       ("(1'(_,/ _'))")
    2.13  
    2.14 -  "_pttrn"      :: [pttrn, pttrns] => pttrn     ("'(_,/_')")
    2.15 -  ""            :: pttrn => pttrns              ("_")
    2.16 -  "_pttrns"     :: [pttrn, pttrns] => pttrns    ("_,/_")
    2.17 +  "_pattern"    :: [pttrn, patterns] => pttrn    ("'(_,/_')")
    2.18 +  ""            :: pttrn => patterns             ("_")
    2.19 +  "_patterns"   :: [pttrn, patterns] => patterns ("_,/_")
    2.20  
    2.21 -  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3SIGMA _:_./ _)" 10)
    2.22 +  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
    2.23    "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
    2.24  
    2.25  translations
    2.26 @@ -65,7 +65,7 @@
    2.27    "A Times B"   => "Sigma A (_K B)"
    2.28  
    2.29  syntax (symbols)
    2.30 -  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
    2.31 +  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
    2.32    "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
    2.33  
    2.34  
     3.1 --- a/src/HOL/W0/Maybe.thy	Mon Sep 22 17:31:28 1997 +0200
     3.2 +++ b/src/HOL/W0/Maybe.thy	Mon Sep 22 17:31:57 1997 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4    bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
     3.5    "m bind f == case m of Ok r => f r | Fail => Fail"
     3.6  
     3.7 -syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
     3.8 +syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
     3.9  translations "P := E; F" == "E bind (%P.F)"
    3.10  
    3.11  end
     4.1 --- a/src/ZF/ZF.thy	Mon Sep 22 17:31:28 1997 +0200
     4.2 +++ b/src/ZF/ZF.thy	Mon Sep 22 17:31:57 1997 +0200
     4.3 @@ -82,7 +82,7 @@
     4.4  
     4.5  types
     4.6    is
     4.7 -  pttrns
     4.8 +  patterns
     4.9  
    4.10  syntax
    4.11    ""          :: i => is                   ("_")
    4.12 @@ -105,9 +105,9 @@
    4.13  
    4.14    (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
    4.15  
    4.16 -  "@pttrn"  :: pttrns => pttrn            ("<_>")
    4.17 -  ""        ::  pttrn           => pttrns ("_")
    4.18 -  "@pttrns" :: [pttrn,pttrns]   => pttrns ("_,/_")
    4.19 +  "@pattern"  :: patterns => pttrn         ("<_>")
    4.20 +  ""          :: pttrn => patterns         ("_")
    4.21 +  "@patterns" :: [pttrn, patterns] => patterns  ("_,/_")
    4.22  
    4.23  translations
    4.24    "x ~: y"      == "~ (x : y)"
    4.25 @@ -151,7 +151,7 @@
    4.26    "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists> _\\<in>_./ _)" 10)
    4.27  (*
    4.28    "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
    4.29 -  "@pttrn"    :: pttrns => pttrn           ("\\<langle>_\\<rangle>")
    4.30 +  "@pattern"  :: patterns => pttrn         ("\\<langle>_\\<rangle>")
    4.31  *)
    4.32  
    4.33