
diff -r 5c1e6b896ff0 -r 2c95d0436a2b IntEx.thy
--- 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




