1signature PairedLambda =
2sig
3 include Abbrev
4
5 val PAIRED_BETA_CONV : conv
6 val PAIRED_ETA_CONV : conv
7 val GEN_BETA_CONV : conv
8 val let_CONV : conv
9 val GEN_LET_CONV : conv
10 val LET_SIMP_CONV : bool -> conv
11
12 val GEN_BETA_RULE : thm -> thm
13 val GEN_BETA_TAC : tactic
14end
15