updated;

GPLed;

write_keywords: string argument (logic name);

isatool unsymbolize;

Modified to make the files build with the new changes in ZF

depends on Epsilon!

fix_frees: rev;

prove: raise ERROR_MESSAGE;

updated;

* ZF: new-style theory commands '(co)inductive', '(co)datatype', 'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');

type_solver_tac: use TCSET' to refer to context of goal state (does *not* work with local proof contexts of Isar / new-style locales);

setup DatatypeTactics.setup;

added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);

no handle ERROR;

fixed;

Isar version of 'rep_datatype';

avoid handle _;

added TCSET(') tacticals;

added Term and Tree_Forest (from converted ZF/ex);

TF and Term moved to ZF/Induct;

miniscoping of UN and INT

Added new entry

New files

new theories from Jacques Fleuriot

*** empty log message ***

converted datatype examples moved from ZF/ex to ZF/Induct;

document setup;

removed BT, Data, Enum (see ZF/Induct);

case_names;

added Datatypes, Binary_Trees (from ZF/ex);

Isar attribute and method setup;

fix path prefix;

use proper intr_names (for required case_names); store con_defs, case_eqns, recursor_eqns, free_iffs, free_elims;

added Induct/Binary_Trees.thy, Induct/Datatypes.thy; removed ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy;

tuned;

updated;

adapted primrec/datatype to Isar;

tuned;

store original simps for codegen;

inductive: removed con_defs;

updated;

updated;

* ZF: new-style theory commands 'inductive', 'inductive_cases', and methods 'ind_cases', 'induct_tac', 'case_tac';

ZF specific keywords;

rearranged inductive package for Isar;

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;