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;

added 'case_names' and 'params';

added rule_cases.ML;

export ALLGOALS_RANGE;

added (un)tag_rule;

added Isar/rule_cases.ML;

added isatool mkdir; isatool document -c; isatool usedir -D -c;

isabelle -c: tell ML system to compress output image;

pass -c option;

observe COMPRESS option;

option -c: tell ML system to compress output image;

* isatool mkdir provides easy setup of Isabelle session directories, including proper documents; * generated LaTeX sources are now deleted after successful run (isatool document -c); may retain a copy somewhere else via -D option of isatool usedir; * old-style theories now produce (crude) LaTeX sources as well; * compression of ML heaps images may now be controlled via -c option of isabelle and isatool usedir;

tuned error msg: rows counted from 1;

tidied

tidied

function "remove" and new lemmas for Factorization

new theory ex/Factorization

new lemmas

added simple_args; added 'tactic' method;

argument: include verbatim;

moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;

added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);

rsyncd setup; --delete mode (beware!);

switched to mirroring with rsync server

new Poly/ML setup made default;

induct: "stripped" option;

require NatDef;

REPEAT_ALL_NEW;

added REPEAT_ALL_NEW;

tidied

tidied

new theories UNITY/Detects, UNITY/Reachability

added con_elim_s(olved_)tac; added 'simplified' flag;

mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;

added multi_resolveq, resolveq_tac;

Added Tanja's Detects and Reachability theories. Also changed object-quantifiers to meta-quantifiers in ball_constrains_UN/INT...

improved reasoning about {} and UNIV

join_rules: compatibility check;

token_trans: symbol length;

join induct rules;

added 'prolog' method;

added freeze_all; tuned spacing;

polished version of the Allocator using Rename

tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and installed them by AddIffs, since they are an important special case of equalityE.

project induct rule;

tuned;

test setup;