--- a/Myhill_1.thy	Wed Feb 09 06:09:46 2011 +0000
+++ b/Myhill_1.thy	Wed Feb 09 07:27:30 2011 +0000
@@ -353,6 +353,9 @@
 
 section {* Equational systems *}
 
+
+text {* The two kinds of terms in the rhs of equations. *}
+
 datatype rhs_item = 
    Lam "rexp"            (* Lambda-marker *)
  | Trn "lang" "rexp"     (* Transition *)