|
47698
|
1 |
(* Title: HOL/Tools/Lifting/lifting_util.ML
|
|
|
2 |
Author: Ondrej Kuncar
|
|
|
3 |
|
|
|
4 |
General-purpose functions used by the Lifting package.
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
signature LIFTING_UTIL =
|
|
|
8 |
sig
|
|
|
9 |
val MRSL: thm list * thm -> thm
|
|
47699
|
10 |
val Trueprop_conv: conv -> conv
|
|
47698
|
11 |
end;
|
|
|
12 |
|
|
|
13 |
|
|
|
14 |
structure Lifting_Util: LIFTING_UTIL =
|
|
|
15 |
struct
|
|
|
16 |
|
|
|
17 |
infix 0 MRSL
|
|
|
18 |
|
|
|
19 |
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
|
|
|
20 |
|
|
47699
|
21 |
fun Trueprop_conv cv ct =
|
|
|
22 |
(case Thm.term_of ct of
|
|
|
23 |
Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
|
|
|
24 |
| _ => raise CTERM ("Trueprop_conv", [ct]))
|
|
|
25 |
|
|
47698
|
26 |
end;
|