--- a/Myhill_1.thy	Mon Feb 14 07:42:16 2011 +0000
+++ b/Myhill_1.thy	Mon Feb 14 09:38:18 2011 +0000
@@ -482,10 +482,10 @@
 *}
 
 abbreviation
-  "Test ES \<equiv> card ES \<noteq> 1"
+  "Cond ES \<equiv> card ES \<noteq> 1"
 
 definition 
-  "Solve X ES \<equiv> while Test (Iter X) ES"
+  "Solve X ES \<equiv> while Cond (Iter X) ES"
 
 text {*
   Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},