src/HOL/ex/LocaleGroup.ML
changeset 6024 cb87f103d114
parent 5848 99dea3c24efb
equal deleted inserted replaced
6023:832b9269dedd 6024:cb87f103d114
   137 by (asm_simp_tac (simpset() delsimps [inv_ax1] 
   137 by (asm_simp_tac (simpset() delsimps [inv_ax1] 
   138 		  addsimps [binop_assoc RS sym]) 1);
   138 		  addsimps [binop_assoc RS sym]) 1);
   139 by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1);
   139 by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1);
   140 qed "right_cancellation";
   140 qed "right_cancellation";
   141 
   141 
   142 Close_locale();
   142 Close_locale "groups";
   143 
   143 
   144 (* example what happens if export *)
   144 (* example what happens if export *)
   145 val Left_cancellation = export left_cancellation;
   145 val Left_cancellation = export left_cancellation;