qualify MetaSimplifier;

added dest_conj, dest_concls;

document setup;

added print_induct_rules;

tuned print operation;

tuned;

* moved induct/cases attributes to Pure, added 'print_induct_rules' command;

print_induct_rules;

updated;

Fixed bug in decompose.

Tools/induct_attrib.ML now part of Pure;

Isar/induct_attrib.ML;

*** empty log message ***

moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;

tuned parentheses in relational expressions;

moved linorder_cases to theory Ord;

linorder_cases supersedes linorder_less_split; tuned parentheses in relational expressions;

eta-expansion required for SML/NJ

support non-oriented infix;

tuned;

tuned;

*** 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.

mksimps and mk_eq_True no longer raise THM exception.

Added label for section on terms.

Added documentation for proof terms.

Added TYPE to Pure grammar.

Added \ttlbrack and \ttrbrack.

Added TPHOLs2000 paper about proof terms.

updated;

tuned;

tuned;

- Exchanged % and %%. - Fixed bug in shrink.

- Tuned syntax - proof_of_term: fixed problems with dummy patterns and typing information