1998-12-28 paulson [Mon, 28 Dec 1998 16:59:28 +0100] rev 6053
new inductive, datatype and primrec packages, etc.
src/ZF/AC.thy src/ZF/Bool.ML src/ZF/Datatype.ML src/ZF/Datatype.thy src/ZF/Finite.thy src/ZF/Inductive.ML src/ZF/Inductive.thy src/ZF/InfDatatype.ML src/ZF/IsaMakefile src/ZF/List.ML src/ZF/List.thy src/ZF/Perm.ML src/ZF/ROOT.ML src/ZF/Univ.ML src/ZF/Univ.thy src/ZF/Zorn.ML src/ZF/Zorn.thy src/ZF/add_ind_def.ML src/ZF/add_ind_def.thy src/ZF/cartprod.ML src/ZF/cartprod.thy src/ZF/constructor.ML src/ZF/constructor.thy src/ZF/ind_syntax.ML src/ZF/ind_syntax.thy src/ZF/indrule.ML src/ZF/indrule.thy src/ZF/intr_elim.ML src/ZF/intr_elim.thy src/ZF/mono.ML src/ZF/thy_syntax.ML src/ZF/typechk.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:58:11 +0100] rev 6052
revised datatype definition package
src/ZF/Tools/datatype_package.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:58:00 +0100] rev 6051
revised inductive definition package
src/ZF/Tools/inductive_package.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:57:38 +0100] rev 6050
new primrec package
src/ZF/Tools/primrec_package.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:57:02 +0100] rev 6049
moved from ZF to new subdirectory Tools
src/ZF/Tools/cartprod.ML src/ZF/Tools/typechk.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:56:07 +0100] rev 6048
new theorem update_type
src/ZF/Update.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:54:53 +0100] rev 6047
converted to use new primrec section and update operator
src/ZF/IMP/Com.ML src/ZF/IMP/Com.thy src/ZF/IMP/Denotation.thy src/ZF/IMP/Equiv.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:54:01 +0100] rev 6046
converted to use new primrec section
src/ZF/Coind/ECR.ML src/ZF/Coind/MT.ML src/ZF/Coind/Map.ML src/ZF/Coind/Types.ML src/ZF/Coind/Types.thy src/ZF/Coind/Values.ML src/ZF/Coind/Values.thy src/ZF/Integ/Bin.ML src/ZF/Integ/Bin.thy src/ZF/Resid/Cube.ML src/ZF/Resid/Redex.ML src/ZF/Resid/Redex.thy src/ZF/Resid/Residuals.ML src/ZF/Resid/SubUnion.ML src/ZF/Resid/SubUnion.thy src/ZF/Resid/Substitution.ML src/ZF/Resid/Substitution.thy src/ZF/Resid/Terms.ML src/ZF/Resid/Terms.thy src/ZF/ex/BT.ML src/ZF/ex/BT.thy src/ZF/ex/Limit.ML src/ZF/ex/ListN.ML src/ZF/ex/PropLog.ML src/ZF/ex/PropLog.thy src/ZF/ex/TF.ML src/ZF/ex/TF.thy src/ZF/ex/Term.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:53:24 +0100] rev 6045
fixed comment
src/ZF/ex/ROOT.ML

1998-12-28 paulson [Mon, 28 Dec 1998 16:52:51 +0100] rev 6044
Needs separate theory Primrec_defs due to new inductive defs package
src/ZF/ex/Primrec.ML src/ZF/ex/Primrec.thy src/ZF/ex/Primrec_defs.ML src/ZF/ex/Primrec_defs.thy