fixed infix names in print_translations;
authorwenzelm
Wed, 12 Oct 1994 11:09:11 +0100
changeset 632 f9a3f77f71e8
parent 631 8bc44f7bbab8
child 633 9e4d4f3eb812
fixed infix names in print_translations;
src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed Oct 12 09:48:32 1994 +0100
+++ b/src/ZF/ZF.thy	Wed Oct 12 11:09:11 1994 +0100
@@ -220,5 +220,5 @@
 (* 'Dependent' type operators *)
 
 val print_translation =
-  [("Pi", dependent_tr' ("@PROD", "->")),
-   ("Sigma", dependent_tr' ("@SUM", "*"))];
+  [("Pi", dependent_tr' ("@PROD", "op ->")),
+   ("Sigma", dependent_tr' ("@SUM", "op *"))];