proper close_locale;

no longer support "isabelle_font" or "symbols";

got rid of obsolete input filtering;

back to normal; tuned;

eliminated old "symbols" syntax, use "xsymbols" instead;

updated;

got rid of obsolete input filtering and isabelle font encoding;

got rid of obsolete input filtering;

eliminated old "symbols" syntax, use "xsymbols" instead;

theory data: finish method;

removed needs_filtered_use;

\newcommand{\isasymindex}{\isamath{\i}};

* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.) now consider the syntactic context of assumptions, giving a better chance to get type-inference of the arguments right (this is especially important for locales); * system: refrain from any attempt at filtering input streams; no longer support ``8bit'' encoding of old isabelle font, instead proper iso-latin characters may now be used;

tuned;

\bibliographystyle{abbrv};

updated;

make SML/XL of NJ happy;

ex/document/root.bib;

proper syntax for structs;

more explanations on advanced syntax;

use num_const of Pure;

\newcommand{\isasymstruct}{\isamath{\diamond}};

locale_prefix: Sign.base_name;

syntax for structs;

tuned;

syntax for structures;

tuned impose_hyps;

added structures; tuned;

\isasymstruct;

Sidi Ehmety's port of the fold_set operator and multisets to ZF. Also, fixes to the cancellation simprocs and a few new standard lemmas.

reorganization of the ZF examples

tuned;

cert_def: proper check of args, improved msgs; tuned;

pretty_goals_local: observes context syntax; PureThy.store_thm: locale_prefix;

defines: Thm.def_name, proper check of args;

separate "in" locale vs. ad-hoc context;

goals_limit moved to display.ML;

added goals_limit (from tctical.ML); added pretty_goals_aux, removed excessive variants of print_goals;

use_thy "Locales";

use locales instead of consts/axioms;

* Isar/Pure: proper integration with ``locales''; unlike the original version by Florian Kammueller, Isar locales package high-level proof contexts rather than raw logical ones (e.g. we admit to include attributes everywhere); * Isar/Pure: theory goals now support ad-hoc contexts, which are discharged in the result, as in ``lemma (assumes A and B) K: A .''; syntax coincides with that of a locale body;

activate dead code, make document work;

renamed Sqrt_Irrational.thy to Sqrt.thy;

Locales and simple mathematical structures;

renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy; added ex/Locales.thy;

extend_XXX: sane argument order ... -> syntax -> syntax;

local syntax: add_syntax, proper read/pretty functions;

locale_element/uses: string;

proper treatment of local syntax; store_thm: test atts; Uses: string;

print_syntax: include local version;

added pretty_term', read_typ', read_typ_no_norm', read_def_terms' which refer to local syntax;

export pretty_thm_aux;

tuned;

theorem(_i): locale atts; global_goal, finish_global: proper treatment of target locale;

group locale_element;

added add_locale(_i) and store_thm; removed old scope stuff; tuned;

theorem(_i): locale atts; added add_locale;

added 'locale', 'print_locales', 'print_locale';

added print_locales, print_locale;

added "locale", "print_locale", "print_locales";

fixes: optional typ; removed garbage;

added pretty/print functions with context; added cert_def; print_asms covers both fixes and assumes;

locale_element: optional typ;

pretty/print functions with context;

export add_tvarsT, add_tvars, add_vars, add_frees (would actually belong to term.ML, but is apt to cause some confusion with the fold-right versions there);

Method.trace ctxt;

tuned;

new Sqrt example

tuned comment;

simplified Proof.init_state:

added get_thms_with_closure; fix_frees: only new ones;

added locale_element;

locale elements;

theorem(_i): locale elements;

locale syntax;

IsarThy.theorem_i (None, []);

updated;

Fixed bug in function add_npvars.

updated;

tuned;

proper use of bind_thm(s);

adapted to new-style theories;

GPLed;

converted theory Dnat;

* 'domain' package adapted to new-style theories, e.g. see HOLCF/ex/Dnat.thy;

document setup;

replaced Undef by UU;

ax_flat;

GPLed;

tuned;

replaced Undef by UU;

converted theory Lift;

rep_datatype lift; converted to new-style theory;

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;