Removed setsubgoaler hack.
--- 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]