# HG changeset patch # User wenzelm # Date 781956551 -3600 # Node ID f9a3f77f71e84aebb4d78260c00896e1785df25e # Parent 8bc44f7bbab825c6d165306aa86f54f98d929017 fixed infix names in print_translations; diff -r 8bc44f7bbab8 -r f9a3f77f71e8 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 *"))];