Structure inttoTacs

Source File	Identifier index	Theory binding index

(* File: inttoTacs.sig  Author: F.L.Morris created 12/13/13 *)

signature inttoTacs =
sig

type conv = Abbrev.conv;
type thm = Thm.thm;
type term = Term.term;
type hol_type = Term.hol_type;
type tactic = Abbrev.tactic;

val intto_CONV: conv;

end;

Source File	Identifier index	Theory binding index

HOL 4, Kananaskis-10