1999-01-12 ago eliminated global/local names;
1998-12-28 ago new inductive, datatype and primrec packages, etc.
1997-12-03 ago Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
1996-05-08 ago Modified to use new functor signatures
1996-01-30 ago expanded tabs
1995-12-22 ago Improving space efficiency of inductive/datatype definitions.
1995-05-03 ago Changed to use split instead of fsplit. The weakening of fsplitE appears not
1994-12-16 ago Defines ZF theory sections (inductive, datatype) at the start/
1994-11-24 ago ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
1994-08-25 ago ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without