src/HOL/Lambda/Commutation.thy
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-02-16 wenzelm 2006-02-16 new-style definitions/abbreviations;
2005-12-23 wenzelm 2005-12-23 tuned proofs;
2005-11-23 wenzelm 2005-11-23 tuned induction proofs;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2002-07-11 berghofe 2002-07-11 Added "using" to the beginning of original newman proof again, because it was lost during last update; renamed second version of newman to newman' (this allows for a comparison of the primitive proof objects, for example).
2002-07-11 nipkow 2002-07-11 Added partly automated version of Newman.
2002-07-11 nipkow 2002-07-11 *** empty log message ***
2002-07-10 wenzelm 2002-07-10 tuned;
2002-04-19 berghofe 2002-04-19 Added proof of Newman's lemma.
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-10-09 nipkow 2000-10-09 added rtranclIs
2000-09-02 wenzelm 2000-09-02 HOL/Lambda: converted into new-style theory and document;
2000-03-30 nipkow 2000-03-30 recdef.rules -> recdef.simps
1997-06-17 nipkow 1997-06-17 converse -> ^-1
1996-02-05 clasohm 1996-02-05 expanded tabs; incorporated Konrad's changes
1995-10-25 nipkow 1995-10-25 Moved some thms to Arith and to Trancl.
1995-10-11 nipkow 1995-10-11 Commutation replaces Confluence