src/HOL/IOA/Solve.thy

     add: executions_def is_execution_fragment_def par_def starts_of_def
     trans_of_def filter_oseq_def
     split add: option.split)
   done
 
-declare split_if [split del] if_weak_cong [cong del]
+declare if_split [split del] if_weak_cong [cong del]
 
 (*Composition of possibility-mappings *)
 lemma fxg_is_weak_pmap_of_product_IOA: 
      "[| is_weak_pmap f C1 A1;  
          externals(asig_of(A1))=externals(asig_of(C1)); 

   apply (rule allI)+
   apply (rule imp_conj_lemma)
   apply (simp (no_asm) add: externals_of_par_extra)
   apply (simp (no_asm) add: par_def)
   apply (simp add: trans_of_def)
-  apply (simplesubst split_if)
+  apply (simplesubst if_split)
   apply (rule conjI)
   apply (rule impI)
   apply (erule disjE)
 (* case 1      a:e(A1) | a:e(A2) *)
   apply (simp add: comp1_reachable comp2_reachable ext_is_act)

   apply (rule impI)
   apply (subgoal_tac "a~:externals (asig_of (A1)) & a~:externals (asig_of (A2))")
 (* delete auxiliary subgoal *)
   prefer 2
   apply force
-  apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
+  apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: if_split)
   apply (tactic {*
     REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE eresolve_tac @{context} [conjE] 1) THEN
       asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *})
   done
 

   apply (rule allI)+
   apply (rule imp_conj_lemma)
   apply (simp (no_asm) add: rename_def)
   apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
   apply safe
-  apply (simplesubst split_if)
+  apply (simplesubst if_split)
   apply (rule conjI)
   apply (rule impI)
   apply (erule disjE)
   apply (erule exE)
   apply (erule conjE)

   apply (erule conjE)
   apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
   apply auto
   done
 
-declare split_if [split] if_weak_cong [cong]
+declare if_split [split] if_weak_cong [cong]
 
 end