Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
authormengj
Fri Oct 28 02:30:12 2005 +0200 (2005-10-28)
changeset 180041883971957de
parent 18003 2aecb2d68c00
child 18005 a444181a45ce
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
src/HOL/Reconstruction.thy
     1.1 --- a/src/HOL/Reconstruction.thy	Fri Oct 28 02:29:01 2005 +0200
     1.2 +++ b/src/HOL/Reconstruction.thy	Fri Oct 28 02:30:12 2005 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  theory Reconstruction
     1.5  imports Hilbert_Choice Map Infinite_Set Extraction
     1.6  uses "Tools/res_clause.ML"
     1.7 +         "Tools/res_hol_clause.ML"
     1.8  	 "Tools/res_axioms.ML"
     1.9  	 "Tools/ATP/recon_order_clauses.ML"
    1.10  	 "Tools/ATP/recon_translate_proof.ML"