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