--- a/src/ZF/ZF.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/ZF.thy Fri Aug 12 12:51:34 1994 +0200
@@ -91,11 +91,11 @@
"`" :: "[i, i] => i" (infixl 90) (*function application*)
(*Except for their translations, * and -> are right and ~: left associative infixes*)
- " *" :: "[i, i] => i" ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
+ "*" :: "[i, i] => i" ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
"Int" :: "[i, i] => i" (infixl 70) (*binary intersection*)
"Un" :: "[i, i] => i" (infixl 65) (*binary union*)
"-" :: "[i, i] => i" (infixl 65) (*set difference*)
- " ->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*)
+ "->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*)
"<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
":" :: "[i, i] => o" (infixl 50) (*membership relation*)
"~:" :: "[i, i] => o" ("(_ ~:/ _)" [50, 51] 50) (*negated membership relation*)
@@ -215,6 +215,6 @@
(* 'Dependent' type operators *)
val print_translation =
- [("Pi", dependent_tr' ("@PROD", " ->")),
- ("Sigma", dependent_tr' ("@SUM", " *"))];
+ [("Pi", dependent_tr' ("@PROD", "->")),
+ ("Sigma", dependent_tr' ("@SUM", "*"))];