--- a/CookBook/Recipes/ExternalSolver.thy	Tue Jan 27 05:41:14 2009 +0000
+++ b/CookBook/Recipes/ExternalSolver.thy	Tue Jan 27 06:15:13 2009 +0000
@@ -25,8 +25,9 @@
   For our explanation here, we will use the @{text metis} prover for proving
   propositional formulae. The general method will be roughly as follows: 
   Given a goal @{text G}, we transform it into the syntactical respresentation 
-  of @{text "metis"}, build the CNF and then let metis search for a refutation. 
-  @{text Metis} will either return the proved goal or raise an exception meaning 
+  of @{text "metis"}, build the CNF of the negated formula and then let metis search 
+  for a refutation. @{text Metis} will either return the proved goal or raise 
+  an exception meaning 
   that it was unable to prove the goal (FIXME: is this so?).
 
   The translation function from Isabelle propositions into formulae of 
@@ -74,7 +75,7 @@
 
   (FIXME: What does Line 8 do?)
 
-  (FIXME: Can this code improved?)
+  (FIXME: Can this code be improved?)
 
 
   Setting up the resolution.
@@ -104,7 +105,7 @@
 
 oracle prop_oracle = prop_dp
 
-text {* (FIXME: What does oracle this do?) *}
+text {* (FIXME: What does oracle do?) *}
 
 
 ML{*fun prop_oracle_tac ctxt = 
@@ -127,9 +128,13 @@
 lemma test: "p \<or> \<not>p"
   by prop_oracle
 
-text {* (FIXME: say something about what the proof of the oracle is) *}
+text {* (FIXME: say something about what the proof of the oracle is)
+
+  @{ML_response_fake [display,gray] "Thm.proof_of @{thm test}" "???"}
 
-ML {* Thm.proof_of @{thm test} *} 
+*} 
+
+
 
 lemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p"
   by prop_oracle