# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264590384 -3600
# Node ID da270d1229652b26c4709a0828cc9cd68c415a40
# Parent  9c3b3eaecaff5f0c78d79cf59e4bf3d0ebdde340
Commenting regularize

diff -r 9c3b3eaecaff -r da270d122965 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 27 08:41:42 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 27 12:06:24 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)