*** empty log message ***

initial setup for chapter on document preparation;

updated output;

- declared wf_java_prog as syntax (previously: definition) - in wf_java_mdecl: added preconditions for 'This' - rule LAss: precondition v ~=This

Removed some unfoldings of defs after declaring wf_java_prog as syntax

Added axiom e~=This to reflect strengthened precond. in rule LAss

Minor modifications

added Ordinals example;

Tuned indentation of abstractions.

tuned;

inductive: no collective atts;

inductive: no collective atts;

oops;

tuned;

recdef (permissive); inductive: no collective atts;

*** empty log message ***

prove: ``strict'' argument;

internal thm numbering with ":" instead of "_";

avoid handle _;

permissive option;

inductive: no collective atts;

updated;

recdef (permissive);

Tuned section about parsing and printing proof terms.