Removed setsubgoaler hack.
authorberghofe
Fri, 01 Jul 2005 14:02:58 +0200
changeset 16638 3dc904d93767
parent 16637 62dff56b43d3
child 16639 5a89d3622ac0
Removed setsubgoaler hack.
src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Fri Jul 01 14:01:13 2005 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Jul 01 14:02:58 2005 +0200
@@ -301,18 +301,10 @@
   "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
   -- {* Beware of argument permutation! *}
 
-ML_setup {* 
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
 lemma (in comm_monoid) finprod_empty [simp]: 
   "finprod G f {} = \<one>"
   by (simp add: finprod_def)
 
-ML_setup {* 
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
 declare funcsetI [intro]
   funcset_mem [dest]