Structure totoTacs

Source File	Identifier index	Theory binding index

(* File: totoTacs.sig  Author: F.L.Morris created 8/20/12 *)

signature totoTacs =
sig

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

val PURE_MATCH_MP: thm -> thm -> thm
val LESS_REWR: thm
val EQUAL_REWR: thm
val GREATER_REWR:thm
val cpn_REWR_CONV: conv

val toto_CONV: thm -> thm -> conv -> conv -> conv
val numto_CONV: conv
val charto_CONV: conv
val qk_numto_CONV: conv
val stringto_CONV: conv

val lextoto_CONV: conv -> conv -> conv
val listoto_CONV: conv -> conv

val numOrd_CONV : conv
val num_pre_CONV : conv

end

Source File	Identifier index	Theory binding index

HOL 4, Trindemossen-1