src/HOL/Tools/res_atp.ML
changeset 16039 dfe264950511
parent 15919 b30a35432f5a
child 16061 8a139c1557bf
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sun May 22 19:26:18 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon May 23 00:18:51 2005 +0200
     1.3 @@ -185,14 +185,14 @@
     1.4                             (* without paramodulation *)
     1.5                             (warning ("goalstring in call_res_tac is: "^goalstring));
     1.6                             (warning ("prob file in cal_res_tac is: "^probfile));
     1.7 -                                                       Watcher.callResProvers(childout,
     1.8 -                            [("spass",thmstr,goalstring,spass_home,  
     1.9 +                                                      (* Watcher.callResProvers(childout,
    1.10 +                            [("spass",thmstr,goalstring,(*spass_home*),  
    1.11                               "-DocProof", 
    1.12 -                             clasimpfile, axfile, hypsfile, probfile)]);
    1.13 +                             clasimpfile, axfile, hypsfile, probfile)]);*)
    1.14  
    1.15                              Watcher.callResProvers(childout,
    1.16 -                            [("spass",thmstr,goalstring,spass_home,  
    1.17 -                             "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    1.18 +                            [("spass",thmstr,goalstring(*,spass_home*),"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/spassshell",  
    1.19 +                             "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    1.20                               clasimpfile, axfile, hypsfile, probfile)]);
    1.21  
    1.22                             (* with paramodulation *)
    1.23 @@ -302,6 +302,7 @@
    1.24          val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
    1.25  
    1.26          (* cq: add write out clasimps to file *)
    1.27 +
    1.28          (* cq:create watcher and pass to isar_atp_aux *)
    1.29          (* tracing *) 
    1.30          (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    1.31 @@ -373,8 +374,8 @@
    1.32  (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
    1.33  (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
    1.34  (*claset file and prob file*)
    1.35 -(* FIX*)
    1.36 -fun isar_local_thms (delta_cs, delta_ss_thms) =
    1.37 +(* FIX: update to work with clausify_axiom_pairs now in ResAxioms*)
    1.38 +(*fun isar_local_thms (delta_cs, delta_ss_thms) =
    1.39      let val thms_cs = get_thms_cs delta_cs
    1.40  	val thms_ss = get_thms_ss delta_ss_thms
    1.41  	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
    1.42 @@ -384,7 +385,7 @@
    1.43      in
    1.44  	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
    1.45      end;
    1.46 -
    1.47 +*)
    1.48  
    1.49  
    1.50  
    1.51 @@ -404,7 +405,7 @@
    1.52            (warning ("initial thm in isar_atp: "^thmstring));
    1.53            (warning ("subgoals in isar_atp: "^prems_string));
    1.54      	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
    1.55 -          (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'"));
    1.56 +          ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
    1.57             isar_atp' (prems, thm))
    1.58      end;
    1.59