src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 48381 1b7d798460bb
parent 48380 d4b7c7be3116
child 48406 b002cc16aa99
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Sledgehammer's iterative relevance filter (MePo = Meng-Paulson).
     1.5  *)
     1.6  
     1.7 -signature SLEDGEHAMMER_FILTER_ITER =
     1.8 +signature SLEDGEHAMMER_MEPO =
     1.9  sig
    1.10    type stature = ATP_Problem_Generate.stature
    1.11    type fact = Sledgehammer_Fact.fact
    1.12 @@ -23,7 +23,7 @@
    1.13      -> term list -> term -> fact list -> fact list
    1.14  end;
    1.15  
    1.16 -structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
    1.17 +structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
    1.18  struct
    1.19  
    1.20  open ATP_Problem_Generate