author | wenzelm |
Tue, 22 Oct 2024 12:45:38 +0200 | |
changeset 81229 | e18600daa904 |
parent 81228 | ed326e93b835 |
child 81230 | fdde6af19ba7 |
--- a/src/Pure/Syntax/mixfix.ML Tue Oct 22 12:41:20 2024 +0200 +++ b/src/Pure/Syntax/mixfix.ML Tue Oct 22 12:45:38 2024 +0200 @@ -1,5 +1,6 @@ (* Title: Pure/Syntax/mixfix.ML - Author: Tobias Nipkow and Markus Wenzel, TU Muenchen + Author: Tobias Nipkow, TU Muenchen + Author: Makarius Mixfix declarations, infixes, binders. *)