1signature Conv = 2sig 3 include Abbrev 4 5 exception UNCHANGED 6 7 val QCONV : conv -> conv 8 val REWR_CONV : thm -> conv 9 val HO_REWR_CONV : thm -> conv 10 val REWR_CONV_A : thm -> conv 11 val LAND_CONV : conv -> conv 12 val RAND_CONV : conv -> conv 13 val RATOR_CONV : conv -> conv 14 val ABS_CONV : conv -> conv 15 val COMB_CONV : conv -> conv 16 val COMB2_CONV : conv * conv -> conv 17 val FORK_CONV : conv * conv -> conv 18 val BINOP_CONV : conv -> conv 19 val EVERY_DISJ_CONV : conv -> conv 20 val EVERY_CONJ_CONV : conv -> conv 21 val QUANT_CONV : conv -> conv 22 val BINDER_CONV : conv -> conv 23 val STRIP_BINDER_CONV : term option -> conv -> conv 24 val STRIP_QUANT_CONV : conv -> conv 25 val LAST_EXISTS_CONV : conv -> conv 26 val LAST_FORALL_CONV : conv -> conv 27 val LHS_CONV : conv -> conv 28 val RHS_CONV : conv -> conv 29 val NO_CONV : conv 30 val ALL_CONV : conv 31 val THENC : conv * conv -> conv 32 val ORELSEC : conv * conv -> conv 33 val IFC : conv -> conv -> conv -> conv 34 val FIRST_CONV : conv list -> conv 35 val EVERY_CONV : conv list -> conv 36 val REPEATC : conv -> conv 37 val CHANGED_CONV : conv -> conv 38 val QCHANGED_CONV : conv -> conv 39 val TRY_CONV : conv -> conv 40 val SUB_CONV : conv -> conv 41 val DEPTH_CONV : conv -> conv 42 val REDEPTH_CONV : conv -> conv 43 val TOP_DEPTH_CONV : conv -> conv 44 val TOP_SWEEP_CONV : conv -> conv 45 val ONCE_DEPTH_CONV : conv -> conv 46 val CONV_RULE : conv -> thm -> thm 47 val HYP_CONV_RULE : (term -> bool) -> conv -> thm -> thm 48 val BETA_RULE : thm -> thm 49 val UNBETA_CONV : term -> conv 50 val NOT_FORALL_CONV : conv 51 val NOT_EXISTS_CONV : conv 52 val EXISTS_NOT_CONV : conv 53 val FORALL_NOT_CONV : conv 54 val FORALL_AND_CONV : conv 55 val EXISTS_OR_CONV : conv 56 val AND_FORALL_CONV : conv 57 val LEFT_AND_FORALL_CONV : conv 58 val RIGHT_AND_FORALL_CONV : conv 59 val OR_EXISTS_CONV : conv 60 val LEFT_OR_EXISTS_CONV : conv 61 val RIGHT_OR_EXISTS_CONV : conv 62 val EXISTS_AND_CONV : conv 63 val EXISTS_AND_REORDER_CONV : conv 64 val AND_EXISTS_CONV : conv 65 val LEFT_AND_EXISTS_CONV : conv 66 val RIGHT_AND_EXISTS_CONV : conv 67 val FORALL_OR_CONV : conv 68 val OR_FORALL_CONV : conv 69 val LEFT_OR_FORALL_CONV : conv 70 val RIGHT_OR_FORALL_CONV : conv 71 val FORALL_IMP_CONV : conv 72 val LEFT_IMP_EXISTS_CONV : conv 73 val RIGHT_IMP_FORALL_CONV : conv 74 val EXISTS_IMP_CONV : conv 75 val BOTH_EXISTS_IMP_CONV : conv 76 val LEFT_IMP_FORALL_CONV : conv 77 val RIGHT_IMP_EXISTS_CONV : conv 78 val X_SKOLEM_CONV : term -> conv 79 val SKOLEM_CONV : conv 80 val SYM_CONV : conv 81 val RIGHT_CONV_RULE : conv -> thm -> thm 82 val FUN_EQ_CONV : conv 83 val X_FUN_EQ_CONV : term -> conv 84 val SELECT_CONV : conv 85 val SPLICE_CONJ_CONV : conv 86 val CONTRAPOS_CONV : conv 87 val ANTE_CONJ_CONV : conv 88 val AND_IMP_INTRO_CONV : conv 89 val SWAP_EXISTS_CONV : conv 90 val SWAP_FORALL_CONV : conv 91 val RESORT_FORALL_CONV : (term list -> term list) -> conv 92 val RESORT_EXISTS_CONV : (term list -> term list) -> conv 93 val FORALL_SIMP_CONV : conv 94 val EXISTS_SIMP_CONV : conv 95 val LIST_FORALL_SIMP_CONV : conv 96 val LIST_FORALL_AND_CONV : conv 97 val LIST_FORALL_IMP_CONV : bool -> conv 98 val LIST_FORALL_OR_CONV : conv 99 val LIST_FORALL_NOT_CONV : conv 100 val MINISCOPE_FORALL_CONV : bool -> conv 101 val LIST_EXISTS_SIMP_CONV : conv 102 val LIST_EXISTS_AND_CONV : conv 103 val LIST_EXISTS_IMP_CONV : bool -> conv 104 val LIST_EXISTS_OR_CONV : conv 105 val LIST_EXISTS_NOT_CONV : conv 106 val MINISCOPE_EXISTS_CONV : bool -> conv 107 val SWAP_VARS_CONV : conv 108 val bool_EQ_CONV : conv 109 val EXISTS_UNIQUE_CONV : conv 110 val COND_CONV : conv 111 val EXISTENCE : thm -> thm 112 val AC_CONV : thm * thm -> conv 113 val GSYM : thm -> thm 114 val RENAME_VARS_CONV : string list -> conv 115 val PAT_CONV : term -> conv -> conv 116 val PRINT_CONV : conv 117 val MAP_THM : conv -> thm -> thm 118 val PATH_CONV : string -> conv -> conv 119 120 val memoize : (term -> 'a option) -> ('a, thm) Redblackmap.dict -> 121 (term -> bool) -> exn -> conv -> conv 122end 123