Removed setsubgoaler hack.
authorberghofe
Fri Jul 01 14:02:58 2005 +0200 (2005-07-01)
changeset 166383dc904d93767
parent 16637 62dff56b43d3
child 16639 5a89d3622ac0
Removed setsubgoaler hack.
src/HOL/Algebra/FiniteProduct.thy
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri Jul 01 14:01:13 2005 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Jul 01 14:02:58 2005 +0200
     1.3 @@ -301,18 +301,10 @@
     1.4    "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
     1.5    -- {* Beware of argument permutation! *}
     1.6  
     1.7 -ML_setup {* 
     1.8 -  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
     1.9 -*}
    1.10 -
    1.11  lemma (in comm_monoid) finprod_empty [simp]: 
    1.12    "finprod G f {} = \<one>"
    1.13    by (simp add: finprod_def)
    1.14  
    1.15 -ML_setup {* 
    1.16 -  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.17 -*}
    1.18 -
    1.19  declare funcsetI [intro]
    1.20    funcset_mem [dest]
    1.21