Thu, 14 Feb 2013 16:17:36 +0100 | wenzelm | tuned proofs; | changeset | files |
Thu, 14 Feb 2013 15:34:33 +0100 | wenzelm | tuned signature -- legacy packages might want to fork proofs as well; | changeset | files |
Thu, 14 Feb 2013 16:01:59 +0100 | Andreas Lochbihler | merged | changeset | files |
Thu, 14 Feb 2013 16:01:28 +0100 | Andreas Lochbihler | implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug | changeset | files |
Thu, 14 Feb 2013 14:14:55 +0100 | haftmann | consolidation of library theories on product orders | changeset | files |
Thu, 14 Feb 2013 12:24:56 +0100 | haftmann | type lifting setup for code numeral types | changeset | files |