[isabelle] Handling failed proof



Hi,

I'm wondering why the exception handling in the following doesn't
behave what I expected to. Does it not try to prove goal1, and if it
fails, it tries to prove goal2? goal2 should be provable, but I still
get a Proof failed exception.

let
  val ctxt = @{context}
  val goal1 = @{prop "EX x y. x > y"}
  val goal2 = @{prop "EX (x::real) y. x > y"}
in
  Goal.prove ctxt [] [] goal1
   (fn _ => auto_tac (clasimpset_of ctxt))
   handle THM _ =>
  Goal.prove ctxt [] [] goal2
   (fn _ => auto_tac (clasimpset_of ctxt))
end;

Thank you for the help.

John





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.