equal
deleted
inserted
replaced
79 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv; |
79 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv; |
80 |
80 |
81 fun try_conv cv = cv else_conv all_conv; |
81 fun try_conv cv = cv else_conv all_conv; |
82 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; |
82 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; |
83 |
83 |
84 fun cache_conv (cv: conv) = Thm.cterm_cache cv; |
84 fun cache_conv (cv: conv) = Ctermtab.cterm_cache cv; |
85 |
85 |
86 |
86 |
87 |
87 |
88 (** Pure conversions **) |
88 (** Pure conversions **) |
89 |
89 |