# HG changeset patch
# User oheimb
# Date 949425516 -3600
# Node ID 879280b505714373c45cd0d6a3a8fa31cee63999
# Parent  6a0b1037bab3e944da79f9eb15bee7d708288783
added forgotten definition of make_imp_tac

diff -r 6a0b1037bab3 -r 879280b50571 src/HOL/IMPP/Com.ML
--- 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";