Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_term.ML
changeset 944 6267ad688ea8
parent 909 3e7a6ec549d1
child 946 46cc6708c3b3 
--- a/Quot/quotient_term.ML	Tue Jan 26 14:08:47 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Jan 26 14:48:25 2010 +0100
@@ -511,6 +511,14 @@
            end
        end 
 
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, Abs(v1', ty', s1))),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , Abs(v2', _  , s2)))) =>
+       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, Abs(v1', ty', regularize_trm ctxt (s1, s2)))
+
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, s1)),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , s2))) =>
+       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, regularize_trm ctxt (s1, s2))
+
   | (t1 $ t2, t1' $ t2') =>
        (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2'))
nominal2