Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
matchess
authorhaftmann
Thu, 25 Sep 2008 09:28:06 +0200
changeset 28348 4f2406ddd9ea
parent 28347 3cb64932ac77
child 28349 46a0dc9b51bb
matchess
src/Pure/pattern.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/pattern.ML	Thu Sep 25 09:28:05 2008 +0200
+++ b/src/Pure/pattern.ML	Thu Sep 25 09:28:06 2008 +0200
@@ -22,6 +22,7 @@
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val matches: theory -> term * term -> bool
+  val matchess: theory -> term list * term list -> bool
   val equiv: theory -> term * term -> bool
   val matches_subterm: theory -> term * term -> bool
   val unify: theory -> term * term -> Envir.env -> Envir.env
@@ -390,6 +391,8 @@
 
 fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
 
+fun matchess thy pos = (fold (match thy) (op ~~ pos) (Vartab.empty, Vartab.empty); true) handle MATCH => false;
+
 fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
isabelle