src/HOL/Tools/res_hol_clause.ML
changeset 32529 d703a76acc08
parent 31910 a8e9ccfc427a
child 32955 4a78daeb012b
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Aug 28 13:32:20 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Sep 04 11:37:24 2009 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    datatype literal = Literal of polarity * combterm
     1.5    datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
     1.6                      kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list}
     1.7 +  val type_of_combterm: combterm -> ResClause.fol_type
     1.8    val strip_comb: combterm -> combterm * combterm list
     1.9    val literals_of_term: theory -> term -> literal list * typ list
    1.10    exception TOO_TRIVIAL