--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Dec 09 04:03:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Dec 09 04:03:30 2013 +0100
@@ -9,6 +9,7 @@
val sledgehammerN : string
val log2 : real -> real
val app_hd : ('a -> 'a) -> 'a list -> 'a list
+ val n_fold_cartesian_product : 'a list list -> 'a list list
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
@@ -48,6 +49,12 @@
fun app_hd f (x :: xs) = f x :: xs
+fun cartesian_product [] _ = []
+ | cartesian_product (x :: xs) yss =
+ map (cons x) yss @ cartesian_product xs yss
+
+fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]]
+
fun plural_s n = if n = 1 then "" else "s"
val serial_commas = Try.serial_commas