adapted to new split order;

--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Jan 07 13:55:29 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Jan 07 13:55:54 1998 +0100
@@ -233,11 +233,11 @@
 by (Asm_full_simp_tac 1);
 
 (* Case y:A, y~:B *)
-by (Seq_case_simp_tac "exB" 1);
+by (Seq_case_simp_tac "exA" 1);
 by (Asm_full_simp_tac 1);
 
 (* Case y~:A, y:B *)
-by (Seq_case_simp_tac "exA" 1);
+by (Seq_case_simp_tac "exB" 1);
 by (Asm_full_simp_tac 1);
 
 (* Case y~:A, y~:B *)
@@ -254,9 +254,9 @@
            Seq_case_simp_tac exA,
            Seq_case_simp_tac exB,
            Asm_full_simp_tac,
-           Seq_case_simp_tac exB,
+           Seq_case_simp_tac exA,
            Asm_full_simp_tac,
-           Seq_case_simp_tac exA,
+           Seq_case_simp_tac exB,
            Asm_full_simp_tac,
            asm_full_simp_tac (simpset() addsimps [asig_of_par,actions_asig_comp])
           ];
@@ -340,7 +340,7 @@
 \ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
 \     Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)";
 
-by (mkex_induct_tac "sch" "exA" "exB");
+by (mkex_induct_tac "sch" "exB" "exA");
 
 qed"filter_mkex_is_exA_tmp";
 
@@ -359,15 +359,6 @@
          lemma for eliminating non admissible equations in assumptions      
   --------------------------------------------------------------------------- *)
 
-(* Versuich 
-goal thy "(y~= nil & Map fst`x <<y) --> x= Zip`y`(Map snd`x)";
-by (Seq_induct_tac "x" [] 1);
-by (Seq_case_simp_tac "y" 2);
-by (pair_tac "a" 1);
-by Auto_tac;
-
-*)
-
 goal thy "!! sch ex. \
 \ Filter (%a. a:act AB)`sch = filter_act`ex  \
 \ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
@@ -414,7 +405,7 @@
 \     Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)";
 
 (* notice necessary change of arguments exA and exB *)
-by (mkex_induct_tac "sch" "exB" "exA");
+by (mkex_induct_tac "sch" "exA" "exB");
 
 qed"filter_mkex_is_exB_tmp";
 
@@ -523,4 +514,4 @@
 
 
 Delsimps compoex_simps;
-Delsimps composch_simps;
\ No newline at end of file
+Delsimps composch_simps;

--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Jan 07 13:55:29 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Jan 07 13:55:54 1998 +0100
@@ -511,8 +511,20 @@
 (* IH *)
 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
+
+(* Case a:A, a~:B *)
+by (forward_tac [divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* filtering internals of A is nil *)
+by (asm_full_simp_tac (simpset() addsimps 
+          [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
+           externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
+by (dres_inst_tac [("x","schA")] subst_lemma1 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
+                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
+
 (* Case a:B, a~:A *)
-
 by (forward_tac [divide_Seq] 1);
 by (REPEAT (etac conjE 1));
 (* filtering internals of A is nil *)
@@ -524,20 +536,8 @@
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
-(* Case a:A, a~:B *)
 
-by (forward_tac [divide_Seq] 1);
-by (REPEAT (etac conjE 1));
-(* filtering internals of A is nil *)
-by (asm_full_simp_tac (simpset() addsimps 
-          [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
-           externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
-by (dres_inst_tac [("x","schA")] subst_lemma1 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
-                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
 (* Case a~:A, a~:B *)
-
 by (fast_tac (claset() addSIs [ext_is_act] 
                       addss (simpset() addsimps [externals_of_par]) ) 1);
 qed"FilterA_mksch_is_tr";