--- a/src/HOL/List.thy Fri Jul 14 16:27:45 2000 +0200
+++ b/src/HOL/List.thy Fri Jul 14 16:28:49 2000 +0200
@@ -43,7 +43,7 @@
"@list" :: args => 'a list ("[(_)]")
(* Special syntax for filter *)
- "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
+ "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_:_./ _])")
(* list update *)
"_lupdbind" :: ['a, 'a] => lupdbind ("(2_ :=/ _)")
--- a/src/HOL/Prod.thy Fri Jul 14 16:27:45 2000 +0200
+++ b/src/HOL/Prod.thy Fri Jul 14 16:28:49 2000 +0200
@@ -49,10 +49,9 @@
syntax
"@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))")
-
- "_pattern" :: [pttrn, patterns] => pttrn ("'(_,/_')")
- "" :: pttrn => patterns ("_")
- "_patterns" :: [pttrn, patterns] => patterns ("_,/_")
+ "_pattern" :: [pttrn, patterns] => pttrn ("'(_,/ _')")
+ "" :: pttrn => patterns ("_")
+ "_patterns" :: [pttrn, patterns] => patterns ("_,/ _")
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80)