added equiv;
authorwenzelm
Tue Jun 13 23:41:49 2006 +0200 (2006-06-13)
changeset 198801b0d48257caf
parent 19879 6a346150611a
child 19881 47937afefdc9
added equiv;
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Tue Jun 13 23:41:47 2006 +0200
     1.2 +++ b/src/Pure/pattern.ML	Tue Jun 13 23:41:49 2006 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    val first_order_match: theory -> term * term
     1.5      -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
     1.6    val matches: theory -> term * term -> bool
     1.7 +  val equiv: theory -> term * term -> bool
     1.8    val matches_subterm: theory -> term * term -> bool
     1.9    val unify: theory -> term * term -> Envir.env -> Envir.env
    1.10    val first_order: term -> bool
    1.11 @@ -405,6 +406,8 @@
    1.12  
    1.13  fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
    1.14  
    1.15 +fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
    1.16 +
    1.17  
    1.18  (* Does pat match a subterm of obj? *)
    1.19  fun matches_subterm thy (pat,obj) =