changeset 6024 | cb87f103d114 |
parent 5848 | 99dea3c24efb |
--- a/src/HOL/ex/LocaleGroup.ML Fri Dec 11 10:38:51 1998 +0100 +++ b/src/HOL/ex/LocaleGroup.ML Fri Dec 11 10:41:53 1998 +0100 @@ -139,7 +139,7 @@ by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1); qed "right_cancellation"; -Close_locale(); +Close_locale "groups"; (* example what happens if export *) val Left_cancellation = export left_cancellation;