# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264591161 -3600
# Node ID fd2493ae3df2321fd66d075d324353ffd1cb9bbc
# Parent  080bd6f1607c11e6e82f51bf8fa9043de8e25baa# Parent  921096706b84ee835018a76e4f05c82da096a714
merged

diff -r 080bd6f1607c -r fd2493ae3df2 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 27 12:19:00 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 27 12:19:21 2010 +0100
@@ -363,6 +363,18 @@
       A = B  ----> (R ===> R) A B
 
    for more complicated types of A and B
+
+
+ The regularize_trm accepts raw theorems in which equalities
+ and quantifiers match exactly the ones in the lifted theorem
+ but also accepts partially regularized terms.
+
+ This means that the raw theorems can have:
+   Ball (Respects R),  Bex (Respects R), Bexeq (Respects R), R
+ in the places where:
+   All, Ex, Ex1, (op =)
+ is required the lifted theorem.
+
 *)
 
 val mk_babs = Const (@{const_name Babs}, dummyT)