2005-06-22 wenzelm [Wed, 22 Jun 2005 19:41:23 +0200] rev 16537
export sort_ord;
tuned term_ord, typ_ord: use pointer_eq;
tuned aconv, aconvs: based on term_ord;
src/Pure/term.ML

2005-06-22 wenzelm [Wed, 22 Jun 2005 19:41:22 +0200] rev 16536
renamed init to init_data;
src/Pure/proofterm.ML src/Pure/pure_thy.ML src/Pure/sign.ML src/Pure/theory.ML

2005-06-22 wenzelm [Wed, 22 Jun 2005 19:41:20 +0200] rev 16535
added structure Object (from Pure/General/object.ML);
src/Pure/library.ML

2005-06-22 wenzelm [Wed, 22 Jun 2005 19:41:19 +0200] rev 16534
tuned;
src/Pure/General/ord_list.ML src/Pure/General/seq.ML src/Pure/display.ML src/Pure/proof_general.ML

2005-06-22 wenzelm [Wed, 22 Jun 2005 19:41:18 +0200] rev 16533
begin_thy: merge maximal imports;
incorporate proof data;
added generic context;
src/Pure/context.ML

2005-06-22 wenzelm [Wed, 22 Jun 2005 19:41:17 +0200] rev 16532
removed Pure/Isar/proof_data.ML, Pure/General/object.ML;
src/Pure/IsaMakefile

2005-06-22 wenzelm [Wed, 22 Jun 2005 19:41:16 +0200] rev 16531
improved proof;
src/HOL/Isar_examples/Drinker.thy

2005-06-22 wenzelm [Wed, 22 Jun 2005 19:41:15 +0200] rev 16530
obsolete (see Pure/context.ML);
src/Pure/General/object.ML src/Pure/Isar/ROOT.ML src/Pure/Isar/proof_data.ML

2005-06-22 wenzelm [Wed, 22 Jun 2005 18:26:28 +0200] rev 16529
tuned;
src/Pure/Isar/isar_thy.ML

2005-06-22 paulson [Wed, 22 Jun 2005 11:20:45 +0200] rev 16528
pointer equality for sml/nj
src/Pure/IsaMakefile src/Pure/ML-Systems/smlnj-ptreql.ML src/Pure/ML-Systems/smlnj.ML