2005-12-17 wenzelm [Sat, 17 Dec 2005 01:00:38 +0100] rev 18427
added sort_distinct;
removed obsolete unique_strings;
src/Pure/library.ML

2005-12-16 urbanc [Fri, 16 Dec 2005 18:22:58 +0100] rev 18426
added container-lemma fresh_eqvt


(definition: container-lemma contains all instantiations
of a lemma from the general theory)
src/HOL/Nominal/nominal_atoms.ML

2005-12-16 urbanc [Fri, 16 Dec 2005 18:20:59 +0100] rev 18425
I think the earlier version was completely broken
(not sure about this one)
src/HOL/Nominal/Examples/Class.thy

2005-12-16 urbanc [Fri, 16 Dec 2005 18:20:03 +0100] rev 18424
tuned more proofs
src/HOL/Nominal/Examples/Fsub.thy

2005-12-16 nipkow [Fri, 16 Dec 2005 16:59:32 +0100] rev 18423
new lemmas
src/HOL/Finite_Set.thy src/HOL/List.thy src/HOL/Set.thy

2005-12-16 haftmann [Fri, 16 Dec 2005 16:00:58 +0100] rev 18422
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
NEWS

2005-12-16 haftmann [Fri, 16 Dec 2005 15:52:05 +0100] rev 18421
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
src/Pure/Isar/isar_thy.ML src/Pure/Isar/locale.ML

2005-12-16 paulson [Fri, 16 Dec 2005 12:15:54 +0100] rev 18420
hashing to eliminate the output of duplicate clauses
src/HOL/IsaMakefile src/HOL/ROOT.ML src/HOL/Tools/ATP/res_clasimpset.ML src/HOL/Tools/res_clause.ML

2005-12-16 paulson [Fri, 16 Dec 2005 11:51:24 +0100] rev 18419
hash tables from SML/NJ
src/Pure/General/hashtable.ML

2005-12-16 haftmann [Fri, 16 Dec 2005 09:00:11 +0100] rev 18418
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
src/HOL/Tools/datatype_package.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/specification_package.ML src/Pure/Isar/attrib.ML src/Pure/Isar/context_rules.ML src/Pure/Isar/isar_thy.ML src/Pure/Isar/method.ML src/Pure/Isar/proof_context.ML src/Pure/axclass.ML src/Pure/pure_thy.ML src/Pure/thm.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/ind_cases.ML src/ZF/Tools/induct_tacs.ML src/ZF/Tools/inductive_package.ML