Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Mon, 07 Sep 2009 22:13:32 +0200
changeset 32540 f97a1e5c9a5a
parent 32538 86035c5f61b5 (diff)
parent 32539 668052c4220e (current diff)
child 32541 cea1716eb106
merged
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Sep 07 22:12:16 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Sep 07 22:13:32 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
isabelle