export RANGE, hard_asm_tac, soft_asm_tac; export is_chain, assert_forward_or_chain; added the_fact; updated ProofContext.export_wrt;

turned into plain context element; exporter setup;

local_def(_i): no constraint on var; exporter setup;

local_def(_i): no constraint on var;

def: no constraint on var;

added is_judgment; removed atomic_thesis;

ObtainFun (generalized existence reasoning);

ThmDeps.enable;

added sign_of_cterm;

Logic.goal_const;

replaced "Sessions" by "Root";

apply. -> by

* HOL/While

added theory While;

export has_internal; tag some rules as internal;

added thm_deps;

added enter_forward_proof;

export write_graph;

begin_theory: store *copy* of initial theory;

tuned;

intro_elim_tac: bimatch_from;

While functional for defining tail-recursive functions

*** empty log message ***

tuned msg;

Corrected example which still used old primrec syntax.

Replaced force by fast because force may now take forever to fail (due to a recend change of David's)

new constant same_fst

by (CLASIMPSET auto_tac);

added clarify method; removed unofficial improper methods;

added clarsimp method;

tuned;

removed slow, slow_best methods; added clarify, clarsimp methods;

* Isar/Provers: intro/elim/dest attributes: changed intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one should have to change intro!! to intro? only);

rearranged setup of arithmetic procedures, avoiding global reference values;

lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);

do nat pass theory value, but sg_ref;

avoid referencing thy value; rename_numerals: use implicit theory context; eliminated some simpset_of Int.thy (why needed anyway?);

avoid referencing thy value; rename_numerals: use implicit theory context;

tuned deps;

tuned;

changed deps;

rename_numerals: use implicit theory context;

avoid referencing thy value; lemma_prat_add_mult_mono moved to PRat.ML;

avoid referencing thy value; lemma_prat_add_mult_mono moved here;

avoid referencing thy value; rename_numerals: use implicit theory context; avoid some simpset_of Int.thy (why needed anyway?);

simpset_of NatDef.thy (why anyway?);

avoid referencing thy value; rename_numerals: use implicit theory context;

avoid referencing thy value;

tuned comment;

avoid global references;

do not pass theory values, but sg_ref;

Drule.merge_rules;

get_names: topologically sorted;

removed all_sessions.graph; improved graph 'directories'; tuned;

removed all_sessions;

disallow duplicates in session identifiers;

assimilated;

tuned HeapFun;

tuned ThmHeap;

removed selector syntax -- improper tuples are broken beyond repair :-(