Thu, 14 Feb 2013 17:58:13 +0100 | Andreas Lochbihler | instantiate finite_UNIV and card_UNIV for finfun type | changeset | files |
Thu, 14 Feb 2013 17:06:15 +0100 | wenzelm | merged | changeset | files |
Thu, 14 Feb 2013 16:36:21 +0100 | wenzelm | more parallel proofs in 'nominal_datatype', although sequential dark matter remains; | changeset | files |