Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Sep 07 19:41:30 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Sep 07 22:08:05 2009 +0200
@@ -68,7 +68,10 @@
    @post v subset s & p(v) &
          forall e in v. ~p(v \ e)
    *)
-  fun minimal p s = min p [] s
+  fun minimal p s =
+    case min p [] s of
+      [x] => if p [] then [] else [x]
+    | m => m
 end