Attempt to patch ACL2 example.

Remove trailing whitespace in source files.

Modified boilerplate for generated ML files, which now end in .sml instead of .ml and have underscores in filenames in place of hyphens.

Continued attemps to add files to examples/M1 ...