--- a/src/Pure/conjunction.ML Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/conjunction.ML Wed Jul 01 21:29:57 2015 +0200
@@ -19,6 +19,7 @@
val intr: thm -> thm -> thm
val intr_balanced: thm list -> thm
val elim: thm -> thm * thm
+ val elim_conjunctions: thm -> thm list
val elim_balanced: int -> thm -> thm list
val curry_balanced: int -> thm -> thm
val uncurry_balanced: int -> thm -> thm
@@ -118,6 +119,11 @@
end;
+fun elim_conjunctions th =
+ (case try elim th of
+ NONE => [th]
+ | SOME (th1, th2) => elim_conjunctions th1 @ elim_conjunctions th2);
+
(* balanced conjuncts *)