Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
authormengj
Sun Jun 04 10:50:41 2006 +0200 (2006-06-04)
changeset 197676e77bd331bf4
parent 19766 031e0dde31f1
child 19768 9afd9b9c47d0
Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
src/HOL/IsaMakefile
src/HOL/Reconstruction.thy
     1.1 --- a/src/HOL/IsaMakefile	Sat Jun 03 17:49:42 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sun Jun 04 10:50:41 2006 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4    Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
     1.5    Tools/ATP/recon_transfer_proof.ML			\
     1.6    Tools/ATP/reduce_axiomsN.ML 							\
     1.7 -  Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
     1.8 +  Tools/ATP/recon_translate_proof.ML 		\
     1.9    Tools/ATP/watcher.ML 					\
    1.10    Tools/cnf_funcs.ML					\
    1.11    Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
     2.1 --- a/src/HOL/Reconstruction.thy	Sat Jun 03 17:49:42 2006 +0200
     2.2 +++ b/src/HOL/Reconstruction.thy	Sun Jun 04 10:50:41 2006 +0200
     2.3 @@ -19,7 +19,6 @@
     2.4  	 "Tools/ATP/AtpCommunication.ML"
     2.5  	 "Tools/ATP/watcher.ML"
     2.6           "Tools/ATP/reduce_axiomsN.ML"
     2.7 -	 "Tools/ATP/res_clasimpset.ML"
     2.8  	 "Tools/res_atp.ML"
     2.9  	 "Tools/reconstruction.ML"
    2.10