src/Pure/pattern.ML
changeset 52127 a40dfe02dd83
parent 51700 c8f2bad67dbb
child 52129 3fd0fe916097
equal deleted inserted replaced
52126:5386150ed067 52127:a40dfe02dd83
    22     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
    22     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
    23   val matches: theory -> term * term -> bool
    23   val matches: theory -> term * term -> bool
    24   val matchess: theory -> term list * term list -> bool
    24   val matchess: theory -> term list * term list -> bool
    25   val equiv: theory -> term * term -> bool
    25   val equiv: theory -> term * term -> bool
    26   val matches_subterm: theory -> term * term -> bool
    26   val matches_subterm: theory -> term * term -> bool
       
    27   val unify_types: theory -> typ * typ -> Envir.env -> Envir.env
    27   val unify: theory -> term * term -> Envir.env -> Envir.env
    28   val unify: theory -> term * term -> Envir.env -> Envir.env
    28   val first_order: term -> bool
    29   val first_order: term -> bool
    29   val pattern: term -> bool
    30   val pattern: term -> bool
    30   val match_rew: theory -> term -> term * term -> (term * term) option
    31   val match_rew: theory -> term -> term * term -> (term * term) option
    31   val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
    32   val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term