changeset 632 | f9a3f77f71e8 |
parent 615 | 84ac5f101bd1 |
child 675 | 59a4fa76b590 |
--- 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 *"))];