--- a/Myhill_1.thy	Fri Feb 11 12:13:35 2011 +0000
+++ b/Myhill_1.thy	Fri Feb 11 13:30:37 2011 +0000
@@ -499,6 +499,8 @@
 where
   "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))"
 
+thm solve.simps
+
 
 text {*
   Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},