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