2006-07-04 berghofe [Tue, 04 Jul 2006 15:20:43 +0200] rev 19985
Implemented proofs of equivariance and finite support
for graph of recursion combinator.
src/HOL/Nominal/nominal_package.ML

2006-07-04 ballarin [Tue, 04 Jul 2006 14:47:01 +0200] rev 19984
Method intro_locales replaced by intro_locales and unfold_locales.
NEWS src/FOL/ex/LocaleTest.thy src/HOL/Algebra/Group.thy src/HOL/Algebra/Lattice.thy src/HOL/Algebra/Module.thy src/HOL/Algebra/UnivPoly.thy src/HOL/Finite_Set.thy src/HOL/Hyperreal/Filter.thy src/HOL/Orderings.thy src/HOL/Real/HahnBanach/FunctionNorm.thy src/HOL/Real/HahnBanach/HahnBanach.thy src/HOL/Real/HahnBanach/NormedSpace.thy src/Pure/Isar/locale.ML

2006-07-04 urbanc [Tue, 04 Jul 2006 12:13:38 +0200] rev 19983
updated
src/HOL/Nominal/INSTALL

2006-07-04 ballarin [Tue, 04 Jul 2006 11:36:08 +0200] rev 19982
Typo.
src/HOL/ex/set.thy

2006-07-04 ballarin [Tue, 04 Jul 2006 11:35:49 +0200] rev 19981
Minor new lemmas.
src/HOL/Algebra/CRing.thy src/HOL/Algebra/Group.thy

2006-07-03 nipkow [Mon, 03 Jul 2006 20:03:11 +0200] rev 19980
replaced respects2 by congruent2 because of type problem
src/HOL/Hyperreal/StarDef.thy

2006-07-03 nipkow [Mon, 03 Jul 2006 20:02:42 +0200] rev 19979
replaced translation by abbreviation
src/HOL/Equiv_Relations.thy

2006-07-03 wenzelm [Mon, 03 Jul 2006 19:33:09 +0200] rev 19978
obtain_export: Thm.generalize;
guess: fixed handling of mixfixes of vars;
tuned;
src/Pure/Isar/obtain.ML

2006-07-03 wenzelm [Mon, 03 Jul 2006 19:33:07 +0200] rev 19977
project_algebra: norm_sort;
tuned;
src/Pure/sorts.ML

2006-07-03 webertj [Mon, 03 Jul 2006 17:27:09 +0200] rev 19976
comments fixed, minor optimization wrt. certifying terms
src/HOL/Tools/sat_funcs.ML