Re: [isabelle] Automating the auto-tools



You'd actually want this:

  nitpick[sat_solver=MiniSat_JNI]
  nitpick[sat_solver=SAT4J]
  apply(auto)
  sledgehammer

Instead of this:

  apply(auto)
  sledgehammer
  nitpick[sat_solver=MiniSat_JNI]
  nitpick[sat_solver=SAT4J]


Since nitpick would only work on the subgoal after the apply(auto).

Regards,
GB






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