Map.empty is now a translation

--- a/src/HOLCF/IOA/ABP/Correctness.ML	Sat Apr 05 17:25:06 2003 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML	Sat Apr 05 22:14:04 2003 +0200
@@ -187,7 +187,7 @@
 
 
 Goal "compatible srch_ioa rsch_ioa"; 
-by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
+by (simp_tac (simpset() addsimps [compatible_def,Int_def]) 1);
 by (rtac set_ext 1);
 by (induct_tac "x" 1);
 by (ALLGOALS(Simp_tac));
@@ -195,7 +195,7 @@
 
 (* totally the same as before *)
 Goal "compatible srch_fin_ioa rsch_fin_ioa"; 
-by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
+by (simp_tac (simpset() addsimps [compatible_def,Int_def]) 1);
 by (rtac set_ext 1);
 by (induct_tac "x" 1);
 by (ALLGOALS(Simp_tac));
@@ -209,7 +209,7 @@
                       Receiver.receiver_trans_def] @ set_lemmas);
 
 Goal "compatible receiver_ioa (srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
 			   actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
@@ -219,7 +219,7 @@
 
 (* 5 proofs totally the same as before *)
 Goal "compatible receiver_ioa (srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
 			actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
@@ -229,7 +229,7 @@
 
 Goal "compatible sender_ioa \
 \      (receiver_ioa || srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
 			actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
@@ -239,7 +239,7 @@
 
 Goal "compatible sender_ioa\
 \      (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def,  compatible_def,asig_of_par,asig_comp_def,
+by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
 				actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
@@ -249,7 +249,7 @@
 
 Goal "compatible env_ioa\
 \      (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
 				actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
@@ -259,7 +259,7 @@
 
 Goal "compatible env_ioa\
 \      (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
 			actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);