1(* wlogLib.sig - Without loss of generality tacticals
2
3For the licensing information about HOL4 see the file "COPYRIGHT" in the
4HOL4 distribution (note added by Mario Castel��n Castro).                   UOK
5
6For the avoidance of legal uncertainty, I (Mario Castel��n Castro) hereby   UOK
7place my modifications to this file in the public domain per the Creative
8Commons CC0 1.0 public domain dedication <https://creativecommons.org/publ
9icdomain/zero/1.0/legalcode>. This should not be interpreted as a personal
10endorsement of permissive (non-Copyleft) licenses. *)
11
12signature wlogLib =
13sig
14  include Abbrev
15
16  val wlog_then : term quotation ->
17                  term quotation list -> thm_tactic -> tactic
18  val wlog_tac  : term quotation -> term quotation list -> tactic
19end
20