src/HOL/NanoJava/TypeRel.thy
2014-01-16 blanchet 2014-01-16 adapted to move of Wfrec
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-08-21 krauss 2011-08-21 modernized specifications
2011-08-11 krauss 2011-08-11 eliminated use of recdef
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-01-16 wenzelm 2011-01-16 tuned headers;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-11 wenzelm 2010-02-11 modernized translations;
2009-05-16 nipkow 2009-05-16 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-16 paulson 2004-06-16 removal of x-symbol syntax <Sigma> for dependent products
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2003-07-25 nipkow 2003-07-25 Replaced \<leadsto> by \<rightharpoonup>
2003-03-17 nipkow 2003-03-17 just a few mods to a few thms
2001-11-22 wenzelm 2001-11-22 renamed "fields" to "flds" (avoid clash with new "fields" operation);
2001-09-28 wenzelm 2001-09-28 recdef (permissive);
2001-09-21 oheimb 2001-09-21 Minor improvements, added Example
2001-09-10 oheimb 2001-09-10 simplified vnam/vname, introduced fname, improved comments
2001-06-16 oheimb 2001-06-16 added NanoJava