1structure pairSimps :> pairSimps = 2struct 3 4open Lib Parse simpLib pairTheory PairedLambda; 5 6 7val PAIR_ss = BasicProvers.thy_ssfrag "pair" 8 9val fvar = ``f:'a -> 'b -> bool``; 10val paired_forall_ss = 11 conv_ss 12 {name = "ELIM_TUPLED_QUANT_CONV (remove paired quantification)", 13 trace = 2, 14 key = SOME ([],``$! (UNCURRY ^fvar)``), 15 conv = K (K pairTools.ELIM_TUPLED_QUANT_CONV)} 16 17val paired_exists_ss = 18 conv_ss 19 {name = "ELIM_TUPLED_QUANT_CONV (remove paired quantification)", 20 trace = 2, 21 key = SOME ([],``$? (UNCURRY ^fvar)``), 22 conv = K (K pairTools.ELIM_TUPLED_QUANT_CONV)} 23 24val gen_beta_ss = 25 conv_ss 26 {name = "GEN_BETA_CONV", 27 trace = 2, 28 key = SOME ([],``(UNCURRY ^fvar) x``), 29 conv = K (K PairedLambda.GEN_BETA_CONV)} 30 31 32 33end (* struct *) 34