src/HOL/Library/Product_ord.thy
2010-08-27 ago renamed class/constant eq to equal; tuned some instantiations
2010-07-12 ago dropped superfluous [code del]s
2010-07-01 ago "prod" and "sum" replace "*" and "+" respectively
2009-05-06 ago compatible with preorder; bot and top instances
2009-03-27 ago normalized imports
2008-10-10 ago `code func` now just `code`
2008-10-07 ago code generator more liberal with respect to sort constraints of instance parameters
2008-06-26 ago established Plain theory and image
2008-05-26 ago tuned theorem order
2007-12-18 ago switched from PreList to ATP_Linkup
2007-12-10 ago switched import from Main to PreList
2007-12-07 ago instantiation target rather than legacy instance
2007-11-29 ago instance command as rudimentary class target
2007-05-06 ago changed code generator invocation syntax
2007-04-20 ago Isar definitions are now added explicitly to code theorem table
2007-03-20 ago added instance for lattice
2007-01-25 ago improved
2006-11-22 ago added code lemmas
2006-05-27 ago tuned;
2005-08-31 ago tuned presentation;
2005-04-15 ago New