# HG changeset patch
# User nipkow
# Date 1252354085 -7200
# Node ID 86035c5f61b56d8174e5ae391da433514b7a0341
# Parent  32e0c39df91d8627eded002651afdfa8b3b055d1
Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)

diff -r 32e0c39df91d -r 86035c5f61b5 src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- 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