moved into Main;

moved String into Main;

tuned;

HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac instead of lift.induct_tac, use UU instead of Undef in cases;

declare transitive;

theory Calculation move to Set;

transitive declared in Pure;

Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.

Goals.add_locale;

fix_frees; improved export_def: handle args on lhs;

theorem: locale argument;

beginnings of new locales (not yet functional);

Goals.setup;

parking code for old-style locales here;

tuned notation (degree instead of dollar);

theorem(_i): locale argument; contexts 0 and 1 in state now refer to theory and locale, respectively; unified export (no longer uses global "standard");

Proof.init_state thy None;

simplified export; tuned printing of fixes;

'atomize': CHANGED_PROP;

global statements: locale argument;

added local_standard;

IsarThy.theorem_i: no locale;

removed obsolete (rule equal_intr_rule);

Additional rules for simplifying inside "Goal"

- Tuned add_cnstrt - Fixed bug in reconstruct_proof that caused infinite loop

Removed name_thm from finish_global.

Tuned function thm_proof.

- enter_thmx -> enter_thms - improved naming of theorems: enter_thms now takes functions pre_name and post_name as arguments

norm_hhf_eq is now stored using open_store_standard_thm.

induct: internalize ``missing'' consumes-facts from goal state (enables unstructured scripts to perform elim-style induction);

- 'induct' may now use elim-style induction rules without chaining facts, using ``missing'' premises from the goal state; this allows rules stemming from inductive sets to be applied in unstructured scripts, while still benefitting from proper handling of non-atomic statements; NB: major inductive premises need to be put first, all the rest of the goal is passed through the induction;

(induct set: ...);

put_consumes: really overwrite existing tag;

finish_global: Tactic.norm_hhf;

use HOL.induct_XXX;

use induct_rulify2;

renamed inductive_XXX to induct_XXX; added induct_impliesI;

induct_impliesI;

tuned induct proofs;

- 'induct' method now derives symbolic cases from the *rulified* rule (before it used to rulify cases stemming from the internal atomized version); this means that the context of a non-atomic statement becomes is included in the hypothesis, avoiding the slightly cumbersome show "PROP ?case" form;

tuned;

induct: cases are extracted from rulified rule;

removed obsolete make_raw;

lemma Least_mono moved from Typedef.thy to Set.thy;

tuned;

removed option -depend (not available everywhere?);

converted theory "Set";

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;

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;