renamed modules
authorblanchet
Fri Oct 22 13:57:54 2010 +0200 (2010-10-22)
changeset 40068ed2869dd9bfa
parent 40067 0783415ed7f0
child 40069 6f7bf79b1506
renamed modules
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 13:54:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 13:57:54 2010 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4    type failure = ATP_Systems.failure
     1.5    type locality = Sledgehammer_Filter.locality
     1.6    type relevance_override = Sledgehammer_Filter.relevance_override
     1.7 -  type fol_formula = Sledgehammer_Translate.fol_formula
     1.8 -  type minimize_command = Sledgehammer_Reconstruct.minimize_command
     1.9 +  type fol_formula = Sledgehammer_ATP_Translate.fol_formula
    1.10 +  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
    1.11  
    1.12    type params =
    1.13      {blocking: bool,
    1.14 @@ -74,8 +74,8 @@
    1.15  open Metis_Translate
    1.16  open Sledgehammer_Util
    1.17  open Sledgehammer_Filter
    1.18 -open Sledgehammer_Translate
    1.19 -open Sledgehammer_Reconstruct
    1.20 +open Sledgehammer_ATP_Translate
    1.21 +open Sledgehammer_ATP_Reconstruct
    1.22  
    1.23  
    1.24  (** The Sledgehammer **)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 13:54:51 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 13:57:54 2010 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  Proof reconstruction for Sledgehammer.
     2.5  *)
     2.6  
     2.7 -signature SLEDGEHAMMER_RECONSTRUCT =
     2.8 +signature SLEDGEHAMMER_ATP_RECONSTRUCT =
     2.9  sig
    2.10    type locality = Sledgehammer_Filter.locality
    2.11    type minimize_command = string list -> string
    2.12 @@ -29,7 +29,7 @@
    2.13    val proof_text : bool -> isar_params -> metis_params -> text_result
    2.14  end;
    2.15  
    2.16 -structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
    2.17 +structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT =
    2.18  struct
    2.19  
    2.20  open ATP_Problem
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 13:54:51 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 13:57:54 2010 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  Translation of HOL to FOL for Sledgehammer.
     3.5  *)
     3.6  
     3.7 -signature SLEDGEHAMMER_TRANSLATE =
     3.8 +signature SLEDGEHAMMER_ATP_TRANSLATE =
     3.9  sig
    3.10    type 'a problem = 'a ATP_Problem.problem
    3.11    type fol_formula
    3.12 @@ -22,7 +22,7 @@
    3.13      -> string problem * string Symtab.table * int * (string * 'a) list vector
    3.14  end;
    3.15  
    3.16 -structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
    3.17 +structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
    3.18  struct
    3.19  
    3.20  open ATP_Problem
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 13:54:51 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 13:57:54 2010 +0200
     4.3 @@ -23,7 +23,6 @@
     4.4  open ATP_Proof
     4.5  open Sledgehammer_Util
     4.6  open Sledgehammer_Filter
     4.7 -open Sledgehammer_Translate
     4.8  open Sledgehammer
     4.9  
    4.10  (* wrapper for calling external prover *)