| Tue, 04 May 2010 12:26:46 +0200 | berghofe | induct_true_def and induct_false_def are already contained in induct_rulify_fallback. | changeset | files |
| Tue, 04 May 2010 11:00:17 +0200 | bulwahn | added lemma about irreflexivity of pointer inequality in Imperative_HOL | changeset | files |
| Tue, 04 May 2010 11:00:16 +0200 | bulwahn | added function ffilter and some lemmas from Finite_Set to the FSet theory | changeset | files |
| Tue, 04 May 2010 10:49:46 +0200 | haftmann | merged | changeset | files |