src/HOL/Equiv_Relations.thy
2010-03-11 haftmann 2010-03-11 Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2009-03-02 nipkow 2009-03-02 name changes
2009-01-28 haftmann 2009-01-28 Plain, Main form meeting points in import hierarchy
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-09-16 haftmann 2008-09-16 dropped superfluous code lemmas
2008-05-07 berghofe 2008-05-07 Instantiated subst rule to avoid problems with HO unification.
2007-11-28 haftmann 2007-11-28 dropped implicit assumption proof
2007-09-26 haftmann 2007-09-26 moved Finite_Set before Datatype
2007-07-10 haftmann 2007-07-10 moved finite lemmas to Finite_Set.thy
2006-12-10 wenzelm 2006-12-10 respects2: tuned spacing;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-07-03 nipkow 2006-07-03 replaced translation by abbreviation
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-03-23 nipkow 2006-03-23 Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
2005-12-22 nipkow 2005-12-22 more lemmas
2005-12-22 nipkow 2005-12-22 new lemmas
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2004-12-09 nipkow 2004-12-09 First step in reorganizing Finite_Set
2004-11-21 nipkow 2004-11-21 added lemmas
2004-11-21 nipkow 2004-11-21 Restructured List and added "rotate"
2004-11-19 paulson 2004-11-19 moved and renamed Integ/Equiv.thy