Lines Matching refs:list
9 val UNFOLD_CONV : (thm list) -> (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
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
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