add_local_context now yields imported and body elements seperatly; additional slight clenup in code

rearranged burrow_split to fold_burrow to allow composition with fold_map

added unfolding(_i); renamed using_thmss(_i) to using_i;

unparse String/AltString: escape quotes;

tuned;

avoid hardwired Trueprop; local proof: static refererence to Pure.thy;

added 'using' command;

updated;

added IsarImplementation;

updated -- lost update!?

* Pure/Isar: new command 'unfolding'; * ML/Provers: more generic wrt. syntax of object-logics; tuned;

ISABELLE_USER for remote cvs access;

outline;

"The Isabelle/Isar Implementation" manual;

* Provers/classical: removed obsolete classical version of elim_format;

tuned forall_intr_vars;

added classical_rule, which replaces Data.make_elim; removed obsolete Data.make_elim and classical elim_format attribute; tuned;

explicitly reject consts *Goal*, *False*;

elim rules: Classical.classical_rule;

removed obsolete cla_dist_concl;

removed classical elim_format;

removed obsolete Provers/make_elim.ML;

obsolete, see classical_rule in Provers/classical.ML;

more robust phantomsection;

require cla_dist_concl, avoid assumptions about concrete syntax;

avoid implicit assumptions about consts Not, op =, *Goal*, *False*;

provide equality_name, not_name;

fixed final_consts;

provide cla_dist_concl;

non-PDF: phantomsection;

added atom keyword

changes in code generator keywords

adaptions to changes in code generator

slight improvements

slightly improved serialization

substantial improvements in code generating

added map_index

tuned proofs;

removed obsolete atomize_old; induct: align_left insts of mutual rules;

removed obsolete induct_atomize_old;

the "skolem" attribute and better initialization of the clause database

blacklist of prolific theorems (must be replaced by an attribute later

tidied

tuned;

* Provers/induct: support simultaneous goals with mutual rules;

induct etc.: admit multiple rules;

backpatching of Substring.full;

goal/qed: proper treatment of two levels of conjunctions;

Logic.mk_conjunction_list; PRECISE_CONJUNCTS: two levels;

turned bicompose_no_flatten into compose_no_flatten, without elimination;

CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;

added mk_conjunction_list2;

conj_elim_precise: proper treatment of nested conjunctions;

Thm.compose_no_flatten;

proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;

is_prefix

slight improvements

more lemmas

shorter proof

Tuned syntax for perm.

new lemmas

Fixed a use of an outdated Substring function

tuned;

exh_casedist2: norm_hhf_eq;

added bicompose_no_flatten, which refrains from changing the shape of the new subgoals;

bicompose_proof: no_flatten;

conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;

Transform mutual rule into projection.

added Provers/project_rule.ML

structure ProjectRule;

* induct: improved treatment of mutual goals and mutual rules;

updated auxiliary facts for induct method; removed dead code;

prop_tr': proper handling of aprop marked as bound;

consume: expand defs in prems of concls; added add_consumes; make/extract_cases: split cases consisting of meta-conjunctions; added mutual_rule;

cases: main is_proper flag; print_cases: show proper cases only;

auto cases: marked improper; tuned;

conjunction_tac: single goal;

CONJUNCTS2;

rule_context: numbered cases;

conjunction_tac: single goal; added CONJUNCTS2, precise_conjunction_tac; removed smart_conjunction_tac;

renamed imp_cong' to imp_cong_rule;

mk_conjunction: proper treatment of bounds; added dest_conjunction(s);

fixed has_internal; added is_internal; renamed imp_cong' to imp_cong_rule; uniform versions of forall_conv, concl_conv, prems_conv, conjunction_conv;

Tactic.precise_conjunction_tac;

added locale meta_conjunction_syntax and various conjunction rules;

simplified setup: removed dest_concls, local_impI, conjI; improved handling of simultaneous goals: split cases; simplified treatment of mutual rules, which are now specified as a list instead of object-level conjunction (cf. set/type/rule); moved join_rules to RuleCases.mutual_rule;

induct_rulify;

actually produce projected rules; *.inducts holds all projected rules;

*.inducts holds all projected rules;

tuned;

tuned induct proofs;

mutual induct with *.inducts;

wf_induct_rule: consumes 1;

structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;

updated auxiliary facts for induct method;

slight improvements