1signature leakageLib =
2sig
3
4   include Abbrev
5
6   val REPEAT_SAFE_EVAL                         : term -> thm
7   val FIND_CONV                                : term -> (term -> thm) -> conv
8   val ONCE_FIND_CONV                           : term -> (term -> thm) -> conv
9   val UNFOLD_CONV                              : (thm list) -> (term -> thm) -> conv
10   val MAKE_ALL_DISTINCT_CONV                   : (term -> thm) -> conv
11   val MEM_CONV                                 : (term -> thm) -> conv
12   val F_UNCHANGED_CONV                         : (term -> thm) -> conv
13   val T_UNCHANGED_CONV                         : (term -> thm) -> conv
14   val T_F_UNCHANGED_CONV                       : (term -> thm) -> conv
15   val LEAKAGE_COMPUTE_PROVE_FINITE             : term -> thm list -> thm
16   val LEAKAGE_COMPUTE_FINITE_HLR               : term * term * term -> thm list -> thm list
17   val LEAKAGE_COMPUTE_CROSS_NOT_EMPTY          : term * term * term -> thm list -> thm
18   val LEAKAGE_COMPUTE_INITIAL_REDUCE           : term * term * term -> thm list -> conv
19   val COMPUTE_CARD                             : term -> (term -> thm) -> (term -> thm) -> thm
20   val COMPUTE_HLR_CARDS                        : term * term * term -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> thm list
21   val LEAKAGE_COMPUTE_REDUCE_CARDS             : term * term * term -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv
22   val LEAKAGE_COMPUTE_HLR_CROSS                : term * term * term -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv
23   val LEAKAGE_COMPUTE_IMAGE_HLR_CROSS          : term * term * term -> thm list -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv
24   val RECURSIVE_UNWIND_SUM                     : (term -> thm) -> (term -> thm) -> term -> thm
25   val LEAKAGE_COMPUTE_UNWIND_OUTER_SUM         : (term -> thm) -> (term -> thm) -> (term -> thm) -> conv
26   val LEAKAGE_COMPUTE_UNWIND_INNER_SUM         : term * term -> thm list -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv
27   val LEAKAGE_COMPUTE_CONV                     : term * term * term -> thm list -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv
28
29end
30