--- a/IntEx.thy	Sat Dec 05 22:38:42 2009 +0100
+++ b/IntEx.thy	Sun Dec 06 00:13:35 2009 +0100
@@ -154,6 +154,9 @@
 abbreviation 
   "Resp \<equiv> Respects"
 
+thm apply_rsp rep_abs_rsp lambda_prs
+ML {* map (Pattern.pattern o bare_concl o prop_of) @{thms apply_rsp rep_abs_rsp lambda_prs} *}
+
 
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})