Remove trailing whitespace in source files.
Small improvements.
Added a Makefile which makes the ACL2 function produced by m1_factorialScript.sml prettier using a special-purpose tool provided by Matt: HOL/examples/acl2/lisp/untranslate-file.lisp
Minor changes.
A decompiler for J's M1 model from ACL2.