Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
authorurbanc
Sat Oct 29 15:01:25 2005 +0200 (2005-10-29)
changeset 18046b7389981170b
parent 18045 6d69a4190eb2
child 18047 3d643b13eb65
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
This means the syntax of the tactics supports_simp and perm_simp
are exactly like simp, namely

(supports_simp add: .... del: ...)

where the add's and del's are optional.
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Oct 29 14:37:32 2005 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Oct 29 15:01:25 2005 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4  
     1.5  
     1.6  fun simp_meth_setup tac =
     1.7 -  Method.only_sectioned_args (Simplifier.simp_modifiers @ Splitter.split_modifiers)
     1.8 +  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
     1.9    (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
    1.10  
    1.11  val perm_eq_meth        = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);