renamed a variable to avoid possible free/bound confusion

a possibly (?) more perspicous simprule in the "simpset" part

now based on "Main", as it should be

deleted unnecessary "simpset" part from recdef

'oops' made proper; removed 'kill_proof' (superceded by 'kill');

intro_classes_tac: REPEAT_ALL_NEW;

tuned comments;

tuned;

obtain; moved pure methods / atts to pure.tex; tuned;

simplified setup; tuned;

pure methods / atts moved here; tactic emulation moved here; oops moved here; history commands; tuned;

tuned;

obtain; help; intro_classes;

parskip 0pt;

tuned; some more stuff;

fixed theory, context typing; defer, prefer; tuned;

tuned;

simplified Proof General setup;

untag: only name arg; fixed trans att syntax; tuned case command;

arith: "!" arg;

x-symbol; Proof General: TACAS 2000;

fixed \OBTAIN;

fixed dep;

arith method: bang arg;

\isamarkupheader: \section;

generic "kill" command;

old_symbol_source: include header;

kill: include kill_proof;

fixed untag;

untag: remove all tags of given name;

no begin_goal marker (interferes with "latex" etc. output; useless anyway?)

next_block: allow in non-goal blocks as well (experimental);

re-ordered the theorems

better error messages, especially for multiple types

Splitter support;

added HOL/PreLIst.thy;

tuned;

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"