isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Sat, 10 Mar 2007 16:31:55 +0100 - Replaced fold by fold_rev to make sure that list of predicate

changeset

berghofe [Sat, 10 Mar 2007 16:31:55 +0100] rev 22434

- Replaced fold by fold_rev to make sure that list of predicate variables pvars (for invariants) is in the correct order - Adapted to new format of datatype descriptor

Sat, 10 Mar 2007 16:28:06 +0100 - Changed format of descriptor contained in nominal_datatype_info

changeset

berghofe [Sat, 10 Mar 2007 16:28:06 +0100] rev 22433

- Changed format of descriptor contained in nominal_datatype_info - Equivariance proof for graph of primrec combinator no longer uses large simpset (more robust).

Sat, 10 Mar 2007 16:25:57 +0100 Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.

changeset

berghofe [Sat, 10 Mar 2007 16:25:57 +0100] rev 22432

Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.

Sat, 10 Mar 2007 16:24:52 +0100 Adapted to changes in definition of SUP.

changeset

berghofe [Sat, 10 Mar 2007 16:24:52 +0100] rev 22431

Adapted to changes in definition of SUP.

Sat, 10 Mar 2007 16:23:28 +0100 Generalized version of SUP and INF (with index set).

changeset

berghofe [Sat, 10 Mar 2007 16:23:28 +0100] rev 22430

Generalized version of SUP and INF (with index set).