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