Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Argo.thy
changeset 69605 a96320074298
parent 63960 3daf02070be5 
--- a/src/HOL/Argo.thy	Sun Jan 06 13:44:33 2019 +0100
+++ b/src/HOL/Argo.thy	Sun Jan 06 15:04:34 2019 +0100
@@ -6,22 +6,22 @@
 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 \<open>~~/src/Tools/Argo/argo_expr.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_term.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_lit.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_proof.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_rewr.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cls.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_common.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cc.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_simplex.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_thy.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_heap.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cdcl.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_core.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_clausify.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_solver.ML\<close>
 
-ML_file "Tools/Argo/argo_tactic.ML"
+ML_file \<open>Tools/Argo/argo_tactic.ML\<close>
 
 end
isabelle