4 |
4 |
5 theory Argo |
5 theory Argo |
6 imports HOL |
6 imports HOL |
7 begin |
7 begin |
8 |
8 |
9 ML_file "~~/src/Tools/Argo/argo_expr.ML" |
9 ML_file \<open>~~/src/Tools/Argo/argo_expr.ML\<close> |
10 ML_file "~~/src/Tools/Argo/argo_term.ML" |
10 ML_file \<open>~~/src/Tools/Argo/argo_term.ML\<close> |
11 ML_file "~~/src/Tools/Argo/argo_lit.ML" |
11 ML_file \<open>~~/src/Tools/Argo/argo_lit.ML\<close> |
12 ML_file "~~/src/Tools/Argo/argo_proof.ML" |
12 ML_file \<open>~~/src/Tools/Argo/argo_proof.ML\<close> |
13 ML_file "~~/src/Tools/Argo/argo_rewr.ML" |
13 ML_file \<open>~~/src/Tools/Argo/argo_rewr.ML\<close> |
14 ML_file "~~/src/Tools/Argo/argo_cls.ML" |
14 ML_file \<open>~~/src/Tools/Argo/argo_cls.ML\<close> |
15 ML_file "~~/src/Tools/Argo/argo_common.ML" |
15 ML_file \<open>~~/src/Tools/Argo/argo_common.ML\<close> |
16 ML_file "~~/src/Tools/Argo/argo_cc.ML" |
16 ML_file \<open>~~/src/Tools/Argo/argo_cc.ML\<close> |
17 ML_file "~~/src/Tools/Argo/argo_simplex.ML" |
17 ML_file \<open>~~/src/Tools/Argo/argo_simplex.ML\<close> |
18 ML_file "~~/src/Tools/Argo/argo_thy.ML" |
18 ML_file \<open>~~/src/Tools/Argo/argo_thy.ML\<close> |
19 ML_file "~~/src/Tools/Argo/argo_heap.ML" |
19 ML_file \<open>~~/src/Tools/Argo/argo_heap.ML\<close> |
20 ML_file "~~/src/Tools/Argo/argo_cdcl.ML" |
20 ML_file \<open>~~/src/Tools/Argo/argo_cdcl.ML\<close> |
21 ML_file "~~/src/Tools/Argo/argo_core.ML" |
21 ML_file \<open>~~/src/Tools/Argo/argo_core.ML\<close> |
22 ML_file "~~/src/Tools/Argo/argo_clausify.ML" |
22 ML_file \<open>~~/src/Tools/Argo/argo_clausify.ML\<close> |
23 ML_file "~~/src/Tools/Argo/argo_solver.ML" |
23 ML_file \<open>~~/src/Tools/Argo/argo_solver.ML\<close> |
24 |
24 |
25 ML_file "Tools/Argo/argo_tactic.ML" |
25 ML_file \<open>Tools/Argo/argo_tactic.ML\<close> |
26 |
26 |
27 end |
27 end |