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