src/HOL/Argo.thy
changeset 63960 3daf02070be5
child 69605 a96320074298
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Argo.thy	Thu Sep 29 20:54:44 2016 +0200
@@ -0,0 +1,27 @@
+(*  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