A Notation for Computer Aided Mathematics
C. L. T. Mannion, Stuart M. Allen · eCommons (Cornell University) · 1994
The NuPrl4 term structure and editor display mechanism are used to provide unambiguous notations for use in the the development of computer supported mathematical arguments. These notations are used to provide a natural statment of a theorem in Hamiltonian dynamics, anchored in a computationally unambiguous representation, that can be made explicit if required.