src/HOL/Lfp.thy
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