Structure intExtensionLib

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

HOL 4, Kananaskis-10