src/HOL/Hoare_Parallel/OG_Tactics.thy

 tactics to control which theorems are used to simplify at each moment,
 so that the original input does not suffer any unexpected
 transformation. *}
 
 lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
-by fast
-lemma list_length: "length []=0 \<and> length (x#xs) = Suc(length xs)"
-by simp
-lemma list_lemmas: "length []=0 \<and> length (x#xs) = Suc(length xs) 
-\<and> (x#xs) ! 0=x \<and> (x#xs) ! Suc n = xs ! n"
-by simp
+  by fast
+
+lemma list_length: "length []=0" "length (x#xs) = Suc(length xs)"
+  by simp_all
+lemma list_lemmas: "length []=0" "length (x#xs) = Suc(length xs)"
+    "(x#xs) ! 0 = x" "(x#xs) ! Suc n = xs ! n"
+  by simp_all
 lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
-by auto
+  by auto
 lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
 lemmas my_simp_list = list_lemmas fst_conv snd_conv
 not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
 Collect_mem_eq ball_simps option.simps primrecdef_list
-lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append list_length
+lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append
 
 ML {*
 fun before_interfree_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm com.simps}, @{thm post.simps}])