1(* wlogLib.sml - Without loss of generality tacticals
2
3   by Mario Castel��n Castro                                                  UOK
4      (see doc/copyrights/public-domain-contributions.txt)
5*)
6
7signature wlogLib =
8sig
9  include Abbrev
10
11  val wlog_then : term quotation ->
12                  term quotation list -> thm_tactic -> tactic
13  val wlog_tac  : term quotation -> term quotation list -> tactic
14end
15