Mon, 26 Apr 2010 21:50:28 +0200 | wenzelm | use 'example_proof' (invisible); | changeset | files |
Mon, 26 Apr 2010 21:45:08 +0200 | wenzelm | command 'example_proof' opens an empty proof body; | changeset | files |
Mon, 26 Apr 2010 21:36:44 +0200 | wenzelm | proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here; | changeset | files |
Mon, 26 Apr 2010 20:30:50 +0200 | wenzelm | eliminanated some unreferenced identifiers; | changeset | files |
Mon, 26 Apr 2010 16:08:04 +0200 | wenzelm | merged | changeset | files |
Mon, 26 Apr 2010 15:14:14 +0200 | Cezary Kaliszyk | add bounded_lattice_bot and bounded_lattice_top type classes | changeset | files |
Mon, 26 Apr 2010 13:43:31 +0200 | haftmann | merged | changeset | files |
Mon, 26 Apr 2010 11:34:19 +0200 | haftmann | dropped group_simps, ring_simps, field_eq_simps | changeset | files |