Made the implementation of 'unless' independent of that of 'co'. This significantly reduces the size of the proof obligations of well-definedness of unless and avoids duplicating the information about unless in the system. The 'except' clause is no longer functional but a test has been added to show that it has to be repaired. It is expected that, with 'unless' separated from 'co', 'except' will reduce rather than increase the burden on the prover.
Implemented the 'except' clauses of 'unless' properties including a coverage of events with indices
Added a module, Document.MachineSpec, for the sole purpose of doing random testing on the machine parser. The properties are still limited but there is a lot one can do with such a module, especially with respect to triggering syntax errors on purpose.