--- 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);