src/HOL/IMP/Transition.thy
2008-01-08 haftmann 2008-01-08 tuned
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-02-07 berghofe 2007-02-07 Adapted to changes in Transitive_Closure theory.
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-01-03 paulson 2006-01-03 Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2001-12-20 nipkow 2001-12-20 renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
2001-12-19 wenzelm 2001-12-19 tuned;
2001-12-09 kleing 2001-12-09 tuned
2001-12-09 kleing 2001-12-09 converted to Isar
2000-07-16 wenzelm 2000-07-16 fixed tuple translations;
2000-07-04 oheimb 2000-07-04 disambiguated := ; added Examples (factorial)
1999-11-24 nipkow 1999-11-24 Basis now Main.
1998-11-13 paulson 1998-11-13 the type of @evalcn was wrong
1998-05-08 wenzelm 1998-05-08 fixed translations;
1998-05-06 nipkow 1998-05-06 Changed [/] to [:=] and removed actual definition.
1998-03-30 oheimb 1998-03-30 removed superfluous translations
1996-06-06 paulson 1996-06-06 Quotes now optional around inductive set
1996-04-29 nipkow 1996-04-29 Streamlined syntax: -(n)-> is now -n->.
1996-04-29 nipkow 1996-04-29 Natural and Transition semantics.