src/HOL/Argo.thy
changeset 63960 3daf02070be5
child 69605 a96320074298
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Argo.thy	Thu Sep 29 20:54:44 2016 +0200
     1.3 @@ -0,0 +1,27 @@
     1.4 +(*  Title:      HOL/Argo.thy
     1.5 +    Author:     Sascha Boehme
     1.6 +*)
     1.7 +
     1.8 +theory Argo
     1.9 +imports HOL
    1.10 +begin
    1.11 +
    1.12 +ML_file "~~/src/Tools/Argo/argo_expr.ML"
    1.13 +ML_file "~~/src/Tools/Argo/argo_term.ML"
    1.14 +ML_file "~~/src/Tools/Argo/argo_lit.ML"
    1.15 +ML_file "~~/src/Tools/Argo/argo_proof.ML"
    1.16 +ML_file "~~/src/Tools/Argo/argo_rewr.ML"
    1.17 +ML_file "~~/src/Tools/Argo/argo_cls.ML"
    1.18 +ML_file "~~/src/Tools/Argo/argo_common.ML"
    1.19 +ML_file "~~/src/Tools/Argo/argo_cc.ML"
    1.20 +ML_file "~~/src/Tools/Argo/argo_simplex.ML"
    1.21 +ML_file "~~/src/Tools/Argo/argo_thy.ML"
    1.22 +ML_file "~~/src/Tools/Argo/argo_heap.ML"
    1.23 +ML_file "~~/src/Tools/Argo/argo_cdcl.ML"
    1.24 +ML_file "~~/src/Tools/Argo/argo_core.ML"
    1.25 +ML_file "~~/src/Tools/Argo/argo_clausify.ML"
    1.26 +ML_file "~~/src/Tools/Argo/argo_solver.ML"
    1.27 +
    1.28 +ML_file "Tools/Argo/argo_tactic.ML"
    1.29 +
    1.30 +end