* Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;

Fixed several bugs concerning arbitrarily branching datatypes.

Eliminated occurrence of rule_format.

tuned;

need at least 3 latex runs to get toc right!

tuned;

tuned;

Rrightarrow;

tuned notation;

tuned notation;

accomodate some recent changes of record package;

updated;

removed "more" sort; refer to properly named theorems internally;

updated records;

'simplified' att: args;

* HOL/record: - removed "more" class (simply use "term") -- INCOMPATIBILITY;

* Provers: 'simplified' attribute may refer to explicit rules instead of full simplifier context; 'iff' attribute handles conditional rules; * HOL/record: - provides cases/induct rules for use with corresponding Isar methods; - old "make" and "make_scheme" operation removed -- INCOMPATIBILITY; - new derived operations "make" (for adding fields of current record), "extend" to promote fixed record to record scheme, and "truncate" for the reverse; cf. theorems "derived_defs", which are *not* declared as simp by default; - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype;

Replaced main proof by proper Isar script.

derived operations are now: make, extend, truncate (cf. derived_defs);

tuned;

check_goal: setmp proofs 0;

added windowlistener (can now close the frame by window controls)

* HOL/record: - provides cases/induct rules for use with corresponding Isar methods; - "record" operation truncates to particular fixed record (acts like a type cast); - make_defs no longer part of default simps; - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype;

innermost_params;