src/HOL/Import/shuffler.ML
changeset 18708 4b3dadb4fe33
parent 18127 9f03d8a9a81b
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4      val add_shuffle_rule: thm -> theory -> theory
     1.5      val shuffle_attr: theory attribute
     1.6  
     1.7 -    val setup      : (theory -> theory) list
     1.8 +    val setup      : theory -> theory
     1.9  end
    1.10  
    1.11  structure Shuffler :> Shuffler =
    1.12 @@ -684,13 +684,15 @@
    1.13  
    1.14  fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm)
    1.15  
    1.16 -val setup = [Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around"),
    1.17 -	     Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems"),
    1.18 -	     ShuffleData.init,
    1.19 -	     add_shuffle_rule weaken,
    1.20 -	     add_shuffle_rule equiv_comm,
    1.21 -	     add_shuffle_rule imp_comm,
    1.22 -	     add_shuffle_rule Drule.norm_hhf_eq,
    1.23 -	     add_shuffle_rule Drule.triv_forall_equality,
    1.24 -	     Attrib.add_attributes [("shuffle_rule",(Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]]
    1.25 +val setup =
    1.26 +  Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
    1.27 +  Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #>
    1.28 +  ShuffleData.init #>
    1.29 +  add_shuffle_rule weaken #>
    1.30 +  add_shuffle_rule equiv_comm #>
    1.31 +  add_shuffle_rule imp_comm #>
    1.32 +  add_shuffle_rule Drule.norm_hhf_eq #>
    1.33 +  add_shuffle_rule Drule.triv_forall_equality #>
    1.34 +  Attrib.add_attributes [("shuffle_rule", (Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]
    1.35 +
    1.36  end