--- a/IntEx.thy	Mon Dec 07 00:13:36 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 01:22:20 2009 +0100
@@ -156,6 +156,8 @@
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 
+thm lambda_prs
+
 lemma test2: "my_plus a = my_plus a"
 apply(rule refl)
 done