1signature PairRules = 2sig 3 include Abbrev 4 5 val MK_PAIR : thm * thm -> thm 6 val PABS : term -> thm -> thm 7 val PABS_CONV : conv -> conv 8 val PSUB_CONV : conv -> conv 9 val CURRY_CONV : conv 10 val UNCURRY_CONV : conv 11 val PBETA_CONV : conv 12 val PBETA_RULE : thm -> thm 13 val PBETA_TAC : tactic 14 val RIGHT_PBETA : thm -> thm 15 val LIST_PBETA_CONV : conv 16 val RIGHT_LIST_PBETA : thm -> thm 17 val LEFT_PBETA : thm -> thm 18 val LEFT_LIST_PBETA : thm -> thm 19 val UNPBETA_CONV : term -> conv 20 val PETA_CONV : conv 21 val PALPHA_CONV : term -> conv 22 val GEN_PALPHA_CONV : term -> conv 23 val PALPHA : term -> term -> thm 24 val paconv : term -> term -> bool 25 val PAIR_CONV : conv -> conv 26 27 val NOT_PFORALL_CONV : conv 28 val NOT_PEXISTS_CONV : conv 29 val PEXISTS_NOT_CONV : conv 30 val PFORALL_NOT_CONV : conv 31 val PFORALL_AND_CONV : conv 32 val PEXISTS_OR_CONV : conv 33 val AND_PFORALL_CONV : conv 34 val LEFT_AND_PFORALL_CONV : conv 35 val RIGHT_AND_PFORALL_CONV : conv 36 val OR_PEXISTS_CONV : conv 37 val LEFT_OR_PEXISTS_CONV : conv 38 val RIGHT_OR_PEXISTS_CONV : conv 39 val PEXISTS_AND_CONV : conv 40 val AND_PEXISTS_CONV : conv 41 val LEFT_AND_PEXISTS_CONV : conv 42 val RIGHT_AND_PEXISTS_CONV : conv 43 val PFORALL_OR_CONV : conv 44 val OR_PFORALL_CONV : conv 45 val LEFT_OR_PFORALL_CONV : conv 46 val RIGHT_OR_PFORALL_CONV : conv 47 val PFORALL_IMP_CONV : conv 48 val LEFT_IMP_PEXISTS_CONV : conv 49 val RIGHT_IMP_PFORALL_CONV : conv 50 val PEXISTS_IMP_CONV : conv 51 val LEFT_IMP_PFORALL_CONV : conv 52 val RIGHT_IMP_PEXISTS_CONV : conv 53 54 val CURRY_FORALL_CONV : conv 55 val CURRY_EXISTS_CONV : conv 56 val UNCURRY_FORALL_CONV : conv 57 val UNCURRY_EXISTS_CONV : conv 58 59 val PSPEC : term -> thm -> thm 60 val PSPECL : term list -> thm -> thm 61 val IPSPEC : term -> thm -> thm 62 val IPSPECL : term list -> thm -> thm 63 val PSPEC_PAIR : thm -> term * thm 64 val PSPEC_ALL : thm -> thm 65 val GPSPEC : thm -> thm 66 val PSPEC_TAC : term * term -> tactic 67 val PGEN : term -> thm -> thm 68 val PGENL : term list -> thm -> thm 69 val P_PGEN_TAC : term -> tactic 70 val PGEN_TAC : tactic 71 val FILTER_PGEN_TAC : term -> tactic 72 73 val PEXISTS_CONV : conv 74 val PSELECT_RULE : thm -> thm 75 val PSELECT_CONV : conv 76 val PEXISTS_RULE : thm -> thm 77 val PSELECT_INTRO : thm -> thm 78 val PSELECT_ELIM : thm -> term * thm -> thm 79 val PEXISTS : term * term -> thm -> thm 80 val PCHOOSE : term * thm -> thm -> thm 81 val P_PCHOOSE_THEN : term -> thm_tactical 82 val PCHOOSE_THEN : thm_tactical 83 val P_PCHOOSE_TAC : term -> thm_tactic 84 val PCHOOSE_TAC : thm_tactic 85 val PEXISTS_TAC : term -> tactic 86 val PEXISTENCE : thm -> thm 87 val PEXISTS_UNIQUE_CONV : conv 88 val P_PSKOLEM_CONV : term -> conv 89 val PSKOLEM_CONV : conv 90 91 val PSTRIP_THM_THEN : thm_tactical 92 val PSTRIP_ASSUME_TAC : thm_tactic 93 val PSTRUCT_CASES_TAC : thm_tactic 94 val PSTRIP_GOAL_THEN : thm_tactic -> tactic 95 val FILTER_PSTRIP_THEN : thm_tactic -> term -> tactic 96 val PSTRIP_TAC : tactic 97 val FILTER_PSTRIP_TAC : term -> tactic 98 val PEXT : thm -> thm 99 val P_FUN_EQ_CONV : term -> conv 100 val MK_PABS : thm -> thm 101 val HALF_MK_PABS : thm -> thm 102 val MK_PFORALL : thm -> thm 103 val MK_PEXISTS : thm -> thm 104 val MK_PSELECT : thm -> thm 105 val PFORALL_EQ : term -> thm -> thm 106 val PEXISTS_EQ : term -> thm -> thm 107 val PSELECT_EQ : term -> thm -> thm 108 val LIST_MK_PFORALL : term list -> thm -> thm 109 val LIST_MK_PEXISTS : term list -> thm -> thm 110 val PEXISTS_IMP : term -> thm -> thm 111 val SWAP_PFORALL_CONV : conv 112 val SWAP_PEXISTS_CONV : conv 113 val PART_PMATCH : (term -> term) -> thm -> term -> thm 114 val PMATCH_MP_TAC : thm_tactic 115 val PMATCH_MP : thm -> thm -> thm 116 117 val pvariant : term list -> term -> term 118 119end 120