# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264590403 -3600
# Node ID 921096706b84ee835018a76e4f05c82da096a714
# Parent  da270d1229652b26c4709a0828cc9cd68c415a40# Parent  c009d2535896fcc0a09d7e06b743ba25df2778aa
merge

diff -r c009d2535896 -r 921096706b84 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 27 11:48:04 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 27 12:06:43 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)