Structure tcTacs

Source File	Identifier index	Theory binding index

(* File: tcTacs.sig  Author: F.L.Morris created 9/6/13 *)

signature tcTacs =
sig

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

val FMAP_TO_RELN: thm;

val ENUF_CONV: conv -> term -> conv;

val TC_CONV: conv -> conv;



end;

Source File	Identifier index	Theory binding index

HOL 4, Kananaskis-10