Structure EVAL_quote


Source File Identifier index Theory binding index

signature EVAL_quote =
sig

include Abbrev
val meta_expr : hol_type -> (term -> bool) ->
                {Op1 : (term * term) list, Op2 : (term * term) list,
                 Vars : term, Csts : term} ->
                term list -> {Metamap : term, Poly : term list}

end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1