1signature quantHeuristicsLibFunRemove = 2sig 3 4 include Abbrev 5 6 type quant_fun_remove_arg; 7 8 val QUANT_FUN_REMOVE_CONV : quant_fun_remove_arg list -> conv 9 val QUANT_FUN_REMOVE_ss : quant_fun_remove_arg list -> simpLib.ssfrag 10 11 (* very simple for to state that some function can be remove. 12 First argument is a theorem of the form 13 "IS_REMOVABLE_QUANT_FUN (\x. f x)". 14 It is important, that there is lambda abstraction, but "f x" can be complicated 15 and even contain free variables. 16 17 The string is suffix used for the new variable names and the 18 thm list is a list of rewrite theorems used carefully to bring every(!) 19 occourence of x into an context of the form "f x". *) 20 21 val remove_thm_arg : thm -> string -> thm list -> quant_fun_remove_arg 22 23end 24