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;

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;

javac -depend;

-D generated;

Added "clean" target.

Fixed problem with batch mode layout, which caused an AWT exception when no X11 connection was available.

initBrowser now has additional noAWT argument.

Constructor no longer takes font as an argument.

Moved font settings from TreeNode to TreeBrowser.

Moved font settings from Vertex to GraphView.

deleted the redundant first argument of adjust(a,b)

Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.

New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1, binary numerals in literal arithmetic.

Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.

keep DISPLAY;

updated;

renamed to Typedefs.thy to avoid conflict with main HOL version;

* proper spacing of consecutive markup elements, especially text blocks after section headings;

\newif\ifisamarkup controls spacing of isabeginpar;

improved spacing;

maintain Latex.flag_markup;

flag_markup;

Types/document/Typedefs;

renamed Typedef.thy to Typedefs.thy (former already present in main HOL);

got rid of separate root.tex;

graceful interpretation of -i/-d/-D options; verbose: additional messages/warnings; include document graph;

include document graph;

document graph option;

conditional: bool -> (unit -> unit) -> unit; std_error: string -> unit;