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