--- 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)
--- 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)
--- 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
--- 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>")
*)