added comments

--- a/src/HOL/UNITY/WFair.thy	Fri Jul 17 10:50:01 1998 +0200
+++ b/src/HOL/UNITY/WFair.thy	Fri Jul 17 10:50:28 1998 +0200
@@ -12,6 +12,8 @@
 
 constdefs
 
+  (*This definition specifies weak fairness.  The rest of the theory
+    is generic to all forms of fairness.*)
   transient :: "[('a * 'a)set set, 'a set] => bool"
     "transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A"
 
@@ -32,11 +34,16 @@
     Trans  "[| leadsTo Acts A B;  leadsTo Acts B C |]
 	   ==> leadsTo Acts A C"
 
+    (*Encoding using powerset of the desired axiom
+       (!!A. A : S ==> leadsTo Acts A B) ==> leadsTo Acts (Union S) B
+    *)
     Union  "(UN A:S. {(A,B)}) : Pow (leadsto Acts)
 	   ==> leadsTo Acts (Union S) B"
 
   monos "[Pow_mono]"
 
+
+(*wlt Acts B is the largest set that leads to B*)
 constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
   "wlt Acts B == Union {A. leadsTo Acts A B}"
 

--- a/src/Pure/Thy/thm_database.ML	Fri Jul 17 10:50:01 1998 +0200
+++ b/src/Pure/Thy/thm_database.ML	Fri Jul 17 10:50:28 1998 +0200
@@ -120,6 +120,9 @@
       val As = Logic.strip_assums_hyp gi
   in map (fn A => subst_bounds(frees,A)) As end;
 
+(*returns all those named_thms whose subterm extracted by extract can be
+  instantiated to obj; the list is sorted according to the number of premises
+  and the size of the required substitution.*)
 fun select_match(obj, signobj, named_thms, extract) =
   let fun matches(prop, tsig) =
             case extract prop of