2004-12-08 paulson 2004-12-08 converted Lfp to new-style theory
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2003-08-27 skalberg 2003-08-27 Converted to new style theories.
2001-09-27 wenzelm 2001-09-27 eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-05-18 wenzelm 2000-05-18 fewer consts declared as global;
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1996-03-08 clasohm 1996-03-08 added constdefs section
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1995-11-29 clasohm 1995-11-29 removed quotes from types in consts and syntax sections
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-05-09 nipkow 1995-05-09 Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application