src/HOL/IOA/Solve.ML

       (simpset() addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
                 addsplits [expand_if,split_option_case]) 1);
 qed"comp2_reachable";
 
+Delsplits [expand_if];
 
 (* Composition of possibility-mappings *)
-
 goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
 \               externals(asig_of(A1))=externals(asig_of(C1)) &\
 \               is_weak_pmap g C2 A2 &  \
 \               externals(asig_of(A2))=externals(asig_of(C2)) & \
 \               compat_ioas C1 C2 & compat_ioas A1 A2  |]     \

 by (rtac impI 1);
 by (etac conjE 1);
 by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
 by Auto_tac;
 qed"rename_through_pmap";
+
+Addsplits [expand_if];