src/HOL/IMP/Expr.thy
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes;
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2001-12-19 wenzelm 2001-12-19 tuned;
2001-12-09 kleing 2001-12-09 converted to Isar
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1996-08-08 berghofe 1996-08-08 Simplified primrec definitions.
1996-06-06 paulson 1996-06-06 Quotes now optional around inductive set
1996-05-07 paulson 1996-05-07 Removal of special syntax for -a-> and -b->
1996-04-27 nipkow 1996-04-27 Arithemtic and boolean expressions are now in a separate theory. The commands don not use them directly. Instead they are based on the semantics (rather than the syntax) of expressions.