do not change parindent/parskip;

Isar: splitter support; improved diagnostics; tuned;

Splitter support;

moved "cases" to generic.tex; improved diagnostic commands; history commands; tuned;

tuned;

Named local contexts (cases); Splitter support; tuned;

Added setup for primrec theory data.

get_recdef now returns None instead of raising ERROR.

Added new theory data slot for primrec equations.

Now returns theorems with correct names in derivations.

Eliminated store_clasimp.

- Fixed bug in prove_casedist_thms (proof failed because of name clashes) - Now returns theorems with correct names in derivations

made SML/XL happy;

## -D document;

renamed isabelle env; proper handling of parindent/parskip;

splitter setup;

clasimp: include Splitter;

splitter setup;

tuned comments;

include Splitter.split_modifiers;

added attributes, method modifiers, theory setup;

export change_global_ss, change_local_ss; separate method_setup, includes further modifiers; clear_ss / 'only': remove loopers as well; simp_modifiers: 'add' optional;

removed export_chain;

eliminated toplevel stack;

'pr': modes, optional limit; 'thm' / 'prop' / 'term' / 'typ': modes; removed 'thence';

pr: modes, optional limit; print_thms/prop/term/type: modes;

pretty chunks;

tuned comment;

tuned comments; renamed isabelle env; proper symbol output for "latex" mode;

added pretty_goals(_marker); pretty chunks;

removed Pretty.spc;

use Pretty.str / Pretty.raw_str;

removed lst, strlen, strlen_real, spc, sym; added chunks, raw_str; pass all strings through Symbol.output (beware: this is done at different times for str and spacing/linebreaks!); speedup formatting (uses Buffer.T); tuned;

made links to homepages absolute, avoids trouble with relative links on the homepages

'undo' prints state (again); 'pr' command: optional limit argument;

pr, disable_pr, enable_pr;

silence undo command;

tuned comments;

invoke_case: include attributes;

'cases' and 'induct' methods;

tuned 'case';

added 'case' command; added 'print_facts', 'print_binds', 'print_cases' commands; added 'cases' method; tuned;

added \NEXT;

proper symbol_output for "xsymbols" mode;

replaced exhaust_tac by case_tac;

renamed cases_tac to case_tac;

case_tac now subsumes both boolean and datatype cases;

use cases; tuned;

* HOL: exhaust_tac on datatypes superceded by new case_tac; * ML: PureThy.add_thms/add_axioms/add_defs now return theorems; * Isar/Pure: much better support for case-analysis; * ML: new combinators |>> and |>>>

renamed cases_tac to case_tac;

adapted to new PureThy.add_thms etc.;

removed cases_of; renamed cases_tac to case_tac; tuned to work with basic HOL as well; add_cases_induct: proper case names; adapted to new PureThy.add_thms etc.;

adapted to new PureThy.add_thms etc.; proper handling of case names;

adapted to new PureThy.add_thms etc.; added store_thms_atts;

use HOLogic.Not; export indexify_names;

adapted to new PureThy.add_thms etc.; tuned case names;

adapted to new PureThy.add_thms etc.; prepare induct rule (case names);

export vars_of;

adapted to new PureThy.add_thms etc.; number cases;

added Not;

adapted to new PureThy.add_thms etc.;

tuned;

cases: preserve order;

*** empty log message ***

exhaust -> cases

exhaust_tac -> cases_tac

renamed "f" to "le" and "mset" to "multiset"

fixed the goal statement of sorted_qsort

adapted to new PureThy.add_thms etc.;

add_thms, add_axioms, add_defs: return theorems as well;

added |>> and |>>>;

exhaust->cases

Type.typ_match now uses Vartab instead of association lists.

tidied

now uses recdef instead of "rules"

tidied, and new thm perm_append2_eq

cases_tac

Type.typ_match now uses Vartab instead of association lists.

Type.unify now uses Vartab instead of association lists.

Added function min_key.

Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.

Envir now uses Vartab instead of association lists.

Type.unify and Type.typ_match now use Vartab instead of association lists.

add_cases_induct: produce proper case names;

type descr;

check_case: disallow (T)Vars in invoked case;

quote tag arguments;

more robust case names of induct;

cleaned comment;

nicely tarted up Mutil

renamed to rsync-isabelle;

tuned;

made rsync "official"

mod_less, div_less are now default simprules

moved more lemmas to Convert (transitivity etc)

mod_less, div_less are now default simprules

Factorization

rsync goes "official" (started at boot time)

tuned for completeness of LBV

some more small lemmas

completeness of the lightweight bytecode verifier

added NT case for method invocation

minor adjustments in branch and method invocation for completeness of LBV

updated discussion of compilers

add_cases: omit unnamed;

invoke_case: name assumption;

fixed section syntax;

sect: exlude ":" from parser;

removed tune_names;

tuned ML types; improved translation functions; 'case' command; 'oops' command; "Emulating tactic scripts";

tuned;

added \CASE, \OBTAIN, \SORRY, \OOPS; removed \SUFF;

added dest_global/local_rules; cases/induct: tuned rule selection, always admit insts; accomodate rule case names;

mk_elims, add_cases_induct: name rule cases;

generalized FINDGOAL, HEADGOAL; handling of local contexts: method_cases, invoke_case;

handling of local contexts: print_cases, get_case, add_cases;

added METHOD_CASES, resolveq_cases_tac; removed multi_resolveq; improved 'tactic' method: bind thm(s) function;

added invoke_case;

added 'case' command; added 'print_cases' command;

added print_cases;