src/HOL/Tools/Lifting/lifting_util.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon Apr 23 17:18:18 2012 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Tools/Lifting/lifting_util.ML
+    Author:     Ondrej Kuncar
+
+General-purpose functions used by the Lifting package.
+*)
+
+signature LIFTING_UTIL =
+sig
+  val MRSL: thm list * thm -> thm
+end;
+
+
+structure Lifting_Util: LIFTING_UTIL =
+struct
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+end;