author | wenzelm |
Wed, 12 Oct 1994 11:09:11 +0100 | |
changeset 632 | f9a3f77f71e8 |
parent 631 | 8bc44f7bbab8 |
child 633 | 9e4d4f3eb812 |
src/ZF/ZF.thy | file | annotate | diff | comparison | revisions |
--- 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 *"))];