added forgotten definition of make_imp_tac

--- a/src/HOL/IMPP/Com.ML	Tue Feb 01 18:18:09 2000 +0100
+++ b/src/HOL/IMPP/Com.ML	Tue Feb 01 18:18:36 2000 +0100
@@ -7,6 +7,8 @@
 qed "domD";
 AddSDs [domD];
 
+val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
+
 Goalw [body_def] "finite (dom body)";
 br finite_dom_map_of 1;
 qed "finite_dom_body";