| Tue, 04 May 2010 14:44:30 +0200 | wenzelm | merged | changeset | files |
| Tue, 04 May 2010 14:10:42 +0200 | berghofe | merged | changeset | files |
| Tue, 04 May 2010 14:11:28 +0200 | berghofe | Turned Sem into an inductive definition. | changeset | files |
| Tue, 04 May 2010 12:29:22 +0200 | berghofe | Corrected handling of "for" parameters. | changeset | files |
| 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 |