Mon, 05 Nov 2007 20:50:42 +0100 | wenzelm | simplified LocalTheory.reinit; | changeset | files |
Mon, 05 Nov 2007 20:50:41 +0100 | wenzelm | improved error message for missing predicates; | changeset | files |
Mon, 05 Nov 2007 18:18:39 +0100 | nipkow | added lemmas | changeset | files |
Mon, 05 Nov 2007 17:48:51 +0100 | ballarin | Use of export rather than standard in interpretation. | changeset | files |
Mon, 05 Nov 2007 17:48:34 +0100 | ballarin | Removed inst_morphism'; satisfy_thm avoids compose. | changeset | files |
Mon, 05 Nov 2007 17:48:17 +0100 | ballarin | Interpretation with named equations. | changeset | files |