# HG changeset patch
# User wenzelm
# Date 874942317 -7200
# Node ID 9f9bcce140ce02146d0b80dd6e0a5770a33d0ea3
# Parent  f0396ac63e12ec9c25b677d8079ffee99d308efd
tuned pattern syntax;

diff -r f0396ac63e12 -r 9f9bcce140ce src/HOL/Modelcheck/MCSyn.thy
--- a/src/HOL/Modelcheck/MCSyn.thy	Mon Sep 22 17:31:28 1997 +0200
+++ b/src/HOL/Modelcheck/MCSyn.thy	Mon Sep 22 17:31:57 1997 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Modelcheck/MCSyn.thy
     ID:         $Id$
-    Author:     Olaf M"uller, Jan Philipps, Robert Sandner
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     Copyright   1997  TU Muenchen
 *)
 
@@ -19,10 +19,10 @@
   "? "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
   "ALL " 	:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
   "EX "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
-   "_lambda"	:: [idts, 'a::logic] => 'b::logic	("(3L _./ _)" 10)
+   "_lambda"	:: [pttrns, 'a] => 'b			("(3L _./ _)" 10)
 
-  "_idts"     	:: [pttrn, idts] => idts		("_,/_" [1, 0] 0)
-  "_pttrn"      :: [pttrn, pttrns] => pttrn     	("_,/_" [1, 0] 0)
+  "_idts"     	:: [idt, idts] => idts		        ("_,/_" [1, 0] 0)
+  "_pattern"    :: [pttrn, patterns] => pttrn     	("_,/_" [1, 0] 0)
 
   "Mu "		:: [idts, 'a pred] => 'a pred		("(3[mu _./ _])" 1000)
   "Nu "		:: [idts, 'a pred] => 'a pred		("(3[nu _./ _])" 1000)
diff -r f0396ac63e12 -r 9f9bcce140ce src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Mon Sep 22 17:31:28 1997 +0200
+++ b/src/HOL/Prod.thy	Mon Sep 22 17:31:57 1997 +0200
@@ -39,16 +39,16 @@
 
 (* patterns -- extends pre-defined type "pttrn" used in abstractions *)
 
-types pttrns
+types patterns
 
 syntax
-  "@Tuple"      :: "['a, args] => 'a * 'b"      ("(1'(_,/ _'))")
+  "@Tuple"      :: "['a, args] => 'a * 'b"       ("(1'(_,/ _'))")
 
-  "_pttrn"      :: [pttrn, pttrns] => pttrn     ("'(_,/_')")
-  ""            :: pttrn => pttrns              ("_")
-  "_pttrns"     :: [pttrn, pttrns] => pttrns    ("_,/_")
+  "_pattern"    :: [pttrn, patterns] => pttrn    ("'(_,/_')")
+  ""            :: pttrn => patterns             ("_")
+  "_patterns"   :: [pttrn, patterns] => patterns ("_,/_")
 
-  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3SIGMA _:_./ _)" 10)
+  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
   "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
 
 translations
@@ -65,7 +65,7 @@
   "A Times B"   => "Sigma A (_K B)"
 
 syntax (symbols)
-  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
+  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
   "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
 
 
diff -r f0396ac63e12 -r 9f9bcce140ce src/HOL/W0/Maybe.thy
--- a/src/HOL/W0/Maybe.thy	Mon Sep 22 17:31:28 1997 +0200
+++ b/src/HOL/W0/Maybe.thy	Mon Sep 22 17:31:57 1997 +0200
@@ -14,7 +14,7 @@
   bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
   "m bind f == case m of Ok r => f r | Fail => Fail"
 
-syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
+syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
 translations "P := E; F" == "E bind (%P.F)"
 
 end
diff -r f0396ac63e12 -r 9f9bcce140ce src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon Sep 22 17:31:28 1997 +0200
+++ b/src/ZF/ZF.thy	Mon Sep 22 17:31:57 1997 +0200
@@ -82,7 +82,7 @@
 
 types
   is
-  pttrns
+  patterns
 
 syntax
   ""          :: i => is                   ("_")
@@ -105,9 +105,9 @@
 
   (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
 
-  "@pttrn"  :: pttrns => pttrn            ("<_>")
-  ""        ::  pttrn           => pttrns ("_")
-  "@pttrns" :: [pttrn,pttrns]   => pttrns ("_,/_")
+  "@pattern"  :: patterns => pttrn         ("<_>")
+  ""          :: pttrn => patterns         ("_")
+  "@patterns" :: [pttrn, patterns] => patterns  ("_,/_")
 
 translations
   "x ~: y"      == "~ (x : y)"
@@ -151,7 +151,7 @@
   "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists> _\\<in>_./ _)" 10)
 (*
   "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
-  "@pttrn"    :: pttrns => pttrn           ("\\<langle>_\\<rangle>")
+  "@pattern"  :: patterns => pttrn         ("\\<langle>_\\<rangle>")
 *)