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;

added export_assume, export_presume, export_def (from proof.ML);

moved RANGE to tctical.ML; moved export_assume, export_presume, export_def to proof_context.ML;

added RANGE (from Isar/proof.ML);

print fixed names as plain strings;

eliminated old numerals;

use generic 1 instead of Numeral1; use improved iff declaration; tuned;

eliminated Numeral0;

build option enables most basic browser info (for proper recording of session);

build option;

tuned;

eliminated old numerals;

pass build mode to process;

removed export_thm;

trace_rules: only non-empty;

removed obsolete "exported" att;

replace_dummy_patterns: lift over bounds;

iff: always rotate prems;

apply(simp add: three_def numerals) (* FIXME !? *);

unset DISPLAY (again);

* Pure: removed obsolete 'exported' attribute; * Pure: dummy pattern "_" in is/let is now automatically ``lifted'' over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");

*** empty log message ***

moved object_logic.ML to Isar/object_logic.ML;

moved locale.ML to Isar/locale.ML;

moved goal related stuff to goals.ML;

Display.current_goals_markers;

tuned;

moved prove_goalw_cterm to goals.ML; cleaned up;

moved local defs to proof.ML (for locales);

improved source arrangement of obtain;

rearrange sources for locales;

Display.print_current_goals_fn;

Display.print_goals;

Display.pretty_thms;

qualified names;

make this module appeat late in Pure; moved print_current_goals to display.ML; added quick_and_dirty_prove_goalw_cterm (from Isar/skip_proof.ML); added thm database functions (from Thy/thm_database.ML);

print_goals stuff is back (from locale.ML);

reorganize sources to accomodate locales;

corollary;

quick_and_dirty_prove_goalw_cterm;