src/HOL/ex/Lagrange.thy
2008-03-29 wenzelm replaced 'ML_setup' by 'ML';
2007-11-27 wenzelm challenge by John Harrison: down to 12s (was 17s, was 75s);
2007-06-23 nipkow tuned and renamed group_eq_simps and ring_eq_simps
2007-01-24 wenzelm updated timing;
2006-11-17 wenzelm more robust syntax for definition/abbreviation/notation;
2006-10-01 wenzelm tuned;
2006-05-27 wenzelm tuned;
2005-09-14 wenzelm tuned headers etc.;
2005-07-07 paulson updated comment
2005-06-25 nipkow Changes due to new abel_cancel.ML
2005-06-17 haftmann migrated theory headers to new format
2004-07-20 nipkow ring_1 -> ring
2004-05-11 obua changes made due to new Ring_and_Field theory
2004-04-16 nipkow Moved ring stuff from ex into Ring_and_Field.
2001-06-13 paulson tidied
1998-06-25 paulson Installation of target HOL-Real
1996-11-26 nipkow A bit of commutative ing theory, with a simplification tacxtic and an example.
less more (0) tip