fixed string_of_mixfix;

tuned declaration of rules;

equal_intr_rule already declared in Pure;

rules for meta-level conjunction;

tuned prove;

tuned;

added prove;

declare equal_intr_rule as intro;

tuned prove; added prove_standard;

removed obsolete goal_subclass, goal_arity;

use Tactic.prove;

use Tactic.prove; improved proof of equality rule;

tuned;

* Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity;

updated;

impose hyps on initial goal configuration (prevents res_inst_tac problems);

added "atomize" method;

prove: primitive goal interface for internal use;

added impose_hyps;

exclude field_simps from user-level "simps";

Isar: fixed rep_datatype args;

hardwire qualified const names;

removed "more" class;

moved product cases/induct to theory Datatype;

made new-style theory; tuned;

atomize_conj;

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

(simp add: point.make_def);

provodes induct/cases for use with corresponding Isar methods; "record" operation (acts as type cast); internal field_inducts, field_cases; make_defs no longer declared as simps; fixed printing of fixed records;

further 1.73 changes: added fix_direct, simplified assume interface;

added read_prop_schematic;

simplified ProofContext.assume interface;

moved lambda to Pure/term.ML;

added lambda;

* clasimp: ``iff'' declarations now handle conditional rules as well;

added string_of_mixfix;

print_depth 8 from the very beginning;