| Source File | Identifier index | Theory binding index |
|---|
signature intExtensionLib =
sig
type term = Term.term
type thm = Thm.thm
type goal = Abbrev.goal
type conv = Abbrev.conv
type tactic = Abbrev.tactic
type simpset = simpLib.simpset
(* tactics *)
val INT_SGN_CASES_TAC: term -> tactic
val INT_CALCEQ_TAC: tactic
end
| Source File | Identifier index | Theory binding index |
|---|