1(* ===================================================================== *) 2(* FILE : numLib.sig *) 3(* DESCRIPTION : useful proof support for :num. *) 4(* *) 5(* ===================================================================== *) 6 7 8signature numLib = 9sig 10 include numSyntax 11 12 val EXISTS_LEAST_CONV : conv 13 val EXISTS_GREATEST_CONV : conv 14 val SUC_ELIM_CONV : conv 15 val SUC_TO_NUMERAL_DEFN_CONV : conv 16 val num_CONV : conv 17 18 val SUC_RULE : rule 19 20 val INDUCT_TAC : tactic 21 val completeInduct_on : term quotation -> tactic 22 val measureInduct_on : term quotation -> tactic 23 24 val LEAST_ELIM_TAC : tactic 25 26 val REDUCE_CONV : conv 27 val REDUCE_RULE : thm -> thm 28 val REDUCE_TAC : tactic 29 30 val ARITH_CONV : conv 31 val ARITH_PROVE : conv 32 val ARITH_TAC : tactic 33 34 val BOUNDED_FORALL_CONV : conv -> conv 35 val BOUNDED_EXISTS_CONV : conv -> conv 36 37 val std_ss : simpLib.simpset 38 val arith_ss : simpLib.simpset 39 40 val DECIDE : conv 41 val DECIDE_TAC : tactic 42 43 val prefer_num : unit -> unit 44 val deprecate_num : unit -> unit 45end 46