2006-07-19 ballarin [Wed, 19 Jul 2006 19:25:58 +0200] rev 20168
Reimplemented algebra method; now controlled by attribute.
src/HOL/Algebra/CRing.thy src/HOL/Algebra/Module.thy src/HOL/Algebra/ringsimp.ML

2006-07-19 ballarin [Wed, 19 Jul 2006 19:24:02 +0200] rev 20167
Strict dfs traversal of imported and registered identifiers.
src/Pure/Isar/locale.ML

2006-07-19 haftmann [Wed, 19 Jul 2006 14:16:36 +0200] rev 20166
added map_default, internal restructuring
src/Pure/General/alist.ML

2006-07-19 wenzelm [Wed, 19 Jul 2006 12:12:08 +0200] rev 20165
export is_tid;
src/Pure/Syntax/lexicon.ML

2006-07-19 wenzelm [Wed, 19 Jul 2006 12:12:07 +0200] rev 20164
thm_of_proof: improved generation of variables;
src/Pure/Proof/proofchecker.ML

2006-07-19 wenzelm [Wed, 19 Jul 2006 12:12:06 +0200] rev 20163
Sign.infer_types: Name.context;
FactIndex.add_local: simplified interface;
Variable.constraints_of;
src/Pure/Isar/proof_context.ML

2006-07-19 wenzelm [Wed, 19 Jul 2006 12:12:05 +0200] rev 20162
reorganize declarations (more efficient);
renamed rename_wrt to variant_frees (avoid confusion with Term.rename_wrt_term, which reverses the result);
tuned;
src/Pure/variable.ML

2006-07-19 wenzelm [Wed, 19 Jul 2006 12:12:04 +0200] rev 20161
Name.context for used'';
src/Pure/type_infer.ML

2006-07-19 wenzelm [Wed, 19 Jul 2006 12:12:03 +0200] rev 20160
added variant_frees;
tuned;
src/Pure/term.ML

2006-07-19 wenzelm [Wed, 19 Jul 2006 12:12:02 +0200] rev 20159
tuned;
src/Pure/proofterm.ML