Generic inductive cases facility for (co)inductive definitions.

converted;

tuned;

tuned inductions;

prove: Envir.beta_norm;

new SList theory from Bu Wolff

induct: rule_versions produces localized variants;

empty rule_context for multiple goals;

added empty;

mutual rules declared as ``consumes 0'';

induct_atomize: include atomize_conj (for mutual induction);

Isar: 'induct' proper support for mutual induction involving non-atomic rule statements; Isar/Pure: support multiple simultaneous goal statements;

proper handling of mutual rules (esp. for sets);

lemmas induct_atomize = atomize_conj ...; val local_imp_def = thm "induct_implies_def";

val local_imp_def = thm "induct_implies_def";

ZF/Induct,UNITY

Tidying necessitated by new simprules in equalities.ML

conditional miniscoping equalities now made unconditional

new-style numerals without leading #, along with generic 0 and 1

congc now returns None if congruence rule has no effect.

Renamed some bound variables due to changes in simplifier.

Fixed proof depending on strange behaviour of rename_bvs.

Renamed some bound variables due to changes in simplifier.

present multi_result;

added meta_conjunction_tr';

pure_syntax_output: "_meta_conjunction";

adapted to multiple results;

adapted auto_bind_goal, auto_bind_facts;

added multi_theorem(_i); have, show etc.: multiple statements;

Proof.have_i: multiple statements;

added RAW_METHOD, RAW_METHOD_CASES; METHOD, METHOD_CASES etc.: conjunction_tac;

added add_thmss;

"theorem" etc.: multiple statements;

theorem, have, show etc: multiple statements;

facts: multiple args;

added conjunction_tac;

renamed open_smart_store_thms to smart_store_thms_open; added Syntax.pure_syntax_output;

added mk_conjunction;

added unflat;

added conj_elim_precise, conj_intr_thm;

use Tactic.prove;

tuned;

support co/inductive definitions in new-style theories;

adapted to add_inductive_x;

syntactic declaration of external *and* internal versions of fixes; tuned warn_extra_tfrees;

fixed print_records;

tuned;

theorems case_split = case_split_thm [case_names True False, cases type: o];

Theorems symmetric, reflexive and transitive are now stored with "open" derivations.

Commands prf and full_prf can now also be used to display proof term of current proof state.

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

theory data: finish method;

indexvar_ast_tr (for \<index> placeholder);

removed pure_sym_syntax; allow additional arguments in infixes (maximum priority);

File.use;

added impose_hyps_tac; robustify insts of tactic emulations;

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;