Theory HOL.Argo

(*  Title:      HOL/Argo.thy
    Author:     Sascha Boehme
*)

theory Argo
imports HOL
begin

ML_file ‹~~/src/Tools/Argo/argo_expr.ML›
ML_file ‹~~/src/Tools/Argo/argo_term.ML›
ML_file ‹~~/src/Tools/Argo/argo_lit.ML›
ML_file ‹~~/src/Tools/Argo/argo_proof.ML›
ML_file ‹~~/src/Tools/Argo/argo_rewr.ML›
ML_file ‹~~/src/Tools/Argo/argo_cls.ML›
ML_file ‹~~/src/Tools/Argo/argo_common.ML›
ML_file ‹~~/src/Tools/Argo/argo_cc.ML›
ML_file ‹~~/src/Tools/Argo/argo_simplex.ML›
ML_file ‹~~/src/Tools/Argo/argo_thy.ML›
ML_file ‹~~/src/Tools/Argo/argo_heap.ML›
ML_file ‹~~/src/Tools/Argo/argo_cdcl.ML›
ML_file ‹~~/src/Tools/Argo/argo_core.ML›
ML_file ‹~~/src/Tools/Argo/argo_clausify.ML›
ML_file ‹~~/src/Tools/Argo/argo_solver.ML›

ML_file ‹Tools/Argo/argo_tactic.ML›

end