src/HOL/Tools/res_atp.ML
changeset 20246 fdfe7399e057
parent 20224 9c40a144ee0e
child 20289 ba7a7c56bed5
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Jul 28 18:11:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Jul 28 18:36:24 2006 +0200
     1.3 @@ -36,9 +36,9 @@
     1.4    val hol_const_types_only: unit -> unit
     1.5    val hol_no_types: unit -> unit
     1.6    val hol_typ_level: unit -> ResHolClause.type_level
     1.7 +  val include_all: bool ref
     1.8    val run_relevance_filter: bool ref
     1.9    val run_blacklist_filter: bool ref
    1.10 -  val invoke_atp_ml : ProofContext.context * thm -> unit
    1.11    val add_all : unit -> unit
    1.12    val add_claset : unit -> unit
    1.13    val add_simpset : unit -> unit
    1.14 @@ -139,16 +139,22 @@
    1.15  val include_simpset = ref false;
    1.16  val include_claset = ref false; 
    1.17  val include_atpset = ref true;
    1.18 -val add_all = (fn () => include_all:=true);
    1.19 -val add_simpset = (fn () => include_simpset:=true);
    1.20 -val add_claset = (fn () => include_claset:=true);
    1.21 -val add_clasimp = (fn () => (include_simpset:=true;include_claset:=true));
    1.22 -val add_atpset = (fn () => include_atpset:=true);
    1.23 -val rm_all = (fn () => include_all:=false);
    1.24 -val rm_simpset = (fn () => include_simpset:=false);
    1.25 -val rm_claset = (fn () => include_claset:=false);
    1.26 -val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false));
    1.27 -val rm_atpset = (fn () => include_atpset:=false);
    1.28 +
    1.29 +(*Tests show that follow_defs gives VERY poor results with "include_all"*)
    1.30 +fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
    1.31 +fun rm_all() = include_all:=false;
    1.32 +
    1.33 +fun add_simpset() = include_simpset:=true;
    1.34 +fun rm_simpset() = include_simpset:=false;
    1.35 +
    1.36 +fun add_claset() = include_claset:=true;
    1.37 +fun rm_claset() = include_claset:=false;
    1.38 +
    1.39 +fun add_clasimp() = (include_simpset:=true;include_claset:=true);
    1.40 +fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
    1.41 +
    1.42 +fun add_atpset() = include_atpset:=true;
    1.43 +fun rm_atpset() = include_atpset:=false;
    1.44  
    1.45  
    1.46  (**** relevance filter ****)