equal
deleted
inserted
replaced
273 lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length |
273 lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length |
274 |
274 |
275 ML {* |
275 ML {* |
276 val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"])) |
276 val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"])) |
277 |
277 |
278 val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [thm "split", thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list"))) |
278 val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [@{thm split}, thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list"))) |
279 |
279 |
280 val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list"))) |
280 val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list"))) |
281 *} |
281 *} |
282 |
282 |
283 text {* The following tactic applies @{text tac} to each conjunct in a |
283 text {* The following tactic applies @{text tac} to each conjunct in a |