src/HOL/MicroJava/BV/Listn.thy
2009-07-28 haftmann 2009-07-28 explicit is better than implicit
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2008-07-15 ballarin 2008-07-15 Removed uses of context element includes.
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2007-01-16 haftmann 2007-01-16 renamed locale partial_order to order
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-11-29 paulson 2004-11-29 converted to Isar script, simplifying some results
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-04-02 nipkow 2002-04-02 Started to convert to locales
2002-03-24 kleing 2002-03-24 cleanup + simpler monotonicity
2002-03-03 kleing 2002-03-03 symbolized
2002-02-21 kleing 2002-02-21 new document
2001-12-16 kleing 2001-12-16 exceptions
2001-03-26 nipkow 2001-03-26 simplified proofs
2001-01-16 wenzelm 2001-01-16 renamed Product_Type.split to split_conv;
2000-11-20 kleing 2000-11-20 BCV integration (first step)