(* 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
val Trueprop_conv: conv -> conv
end;
structure Lifting_Util: LIFTING_UTIL =
struct
infix 0 MRSL
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
fun Trueprop_conv cv ct =
(case Thm.term_of ct of
Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
| _ => raise CTERM ("Trueprop_conv", [ct]))
end;