src/HOL/Import/shuffler.ML
changeset 22846 fb79144af9a3
parent 22578 b0eb5652f210
child 22902 ac833b4bb7ee
     1.1 --- a/src/HOL/Import/shuffler.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -75,20 +75,18 @@
     1.4         | _ => raise THM("Not an equality",0,[th]))
     1.5      handle _ => raise THM("Couldn't make object equality",0,[th])
     1.6  
     1.7 -structure ShuffleDataArgs: THEORY_DATA_ARGS =
     1.8 -struct
     1.9 -val name = "HOL/shuffles"
    1.10 -type T = thm list
    1.11 -val empty = []
    1.12 -val copy = I
    1.13 -val extend = I
    1.14 -fun merge _ = Library.gen_union Thm.eq_thm
    1.15 -fun print _ thms =
    1.16 -    Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    1.17 -                                    (map Display.pretty_thm thms))
    1.18 -end
    1.19 +structure ShuffleData = TheoryDataFun
    1.20 +(
    1.21 +  type T = thm list
    1.22 +  val empty = []
    1.23 +  val copy = I
    1.24 +  val extend = I
    1.25 +  fun merge _ = Library.gen_union Thm.eq_thm
    1.26 +)
    1.27  
    1.28 -structure ShuffleData = TheoryDataFun(ShuffleDataArgs)
    1.29 +fun print_shuffles thy =
    1.30 +  Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    1.31 +    (map Display.pretty_thm (ShuffleData.get thy)))
    1.32  
    1.33  val weaken =
    1.34      let
    1.35 @@ -667,8 +665,6 @@
    1.36          Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
    1.37      end
    1.38  
    1.39 -val print_shuffles = ShuffleData.print
    1.40 -
    1.41  fun add_shuffle_rule thm thy =
    1.42      let
    1.43          val shuffles = ShuffleData.get thy
    1.44 @@ -682,9 +678,10 @@
    1.45  val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
    1.46  
    1.47  val setup =
    1.48 -  Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
    1.49 -  Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #>
    1.50 -  ShuffleData.init #>
    1.51 +  Method.add_method ("shuffle_tac",
    1.52 +    Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
    1.53 +  Method.add_method ("search_tac",
    1.54 +    Method.ctxt_args search_meth,"search for suitable theorems") #>
    1.55    add_shuffle_rule weaken #>
    1.56    add_shuffle_rule equiv_comm #>
    1.57    add_shuffle_rule imp_comm #>