diff -r cd7854f2636d -r 02a9b2540eb7 src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Tue Sep 28 13:30:29 2010 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Fri Oct 01 10:23:38 2010 +0200
@@ -166,6 +166,10 @@
 
 functions for greatest common divisor and canceling
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+################################################################################
+##   search Isabelle2009-2/src/HOL/Multivariate_Analysis
+##   Amine Chaieb, Robert Himmelmann, John Harrison.
+################################################################################
 mv_gcd
 factout_
 factout_p_
@@ -3070,6 +3074,10 @@
 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
     []:(rule * (term * term list)) list;
 
+(* pat matched with the current term gives an environment 
+   (or not: hen the Rrls not applied);
+   if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
+   then the Rrls is applied. *)
 val pat = parse_patt thy "?r/?s";
 val pre1 = parse_patt thy "?r is_expanded";
 val pre2 = parse_patt thy "?s is_expanded";
@@ -3218,13 +3226,14 @@
 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
     []:(rule * (term * term list)) list;
 
+(* if each pat* matches with the current term, the Rrls is applied
+   (there are no preconditions to be checked, they are HOLogic.true_const) *)
 val pat0 = parse_patt thy "?r/?s+?u/?v";
 val pat1 = parse_patt thy "?r/?s+?u   ";
 val pat2 = parse_patt thy "?r   +?u/?v";
 val prepat = [([HOLogic.true_const], pat0),
 	      ([HOLogic.true_const], pat1),
 	      ([HOLogic.true_const], pat2)];
-
 in
 
 (*11.02 schnelle L"osung f"ur RL: Bruch auch gek"urzt;
@@ -3362,6 +3371,8 @@
 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
     []:(rule * (term * term list)) list;
 
+(* if each pat* matches with the current term, the Rrls is applied
+   (there are no preconditions to be checked, they are HOLogic.true_const) *)
 val pat0 =  parse_patt thy "?r/?s+?u/?v";
 val pat01 = parse_patt thy "?r/?s-?u/?v";
 val pat1 =  parse_patt thy "?r/?s+?u   ";