Commit f456aeac authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

fixed latex and .bib errors

parent ffad5ea62de0
......@@ -2,7 +2,7 @@ chapter AFP
session Verified_SAT_Based_AI_Planning (AFP) = HOL +
description {* Verified SAT-Based AI Planning *}
options [timeout = 600, document_variants = "document=-theory,/proof,/ML"]
options [timeout = 600]
......@@ -1591,7 +1591,7 @@ proof -
by argo
\<comment> \<open> A technical lemma used in \isanam{cnf_of_encode_goal_state_set}. \<close>
\<comment> \<open> A technical lemma used in \isaname{cnf_of_encode_goal_state_set}. \<close>
private lemma cnf_of_encode_goal_state_set_i:
"cnf ((\<Phi>\<^sub>G \<Pi>) t ) = \<Union>({ cnf (encode_state_variable t
(index (strips_problem.variables_of \<Pi>) v) (((\<Pi>)\<^sub>G) v))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment