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