--- a/src/HOL/Bali/AxExample.thy Wed May 26 16:17:30 2010 +0200
+++ b/src/HOL/Bali/AxExample.thy Wed May 26 16:28:55 2010 +0200
@@ -189,7 +189,7 @@
apply (tactic "ax_tac 1")
apply (rule_tac [2] ax_subst_Var_allI)
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
-apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
apply (tactic "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac 3")
--- a/src/HOL/Hoare/hoare_tac.ML Wed May 26 16:17:30 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Wed May 26 16:28:55 2010 +0200
@@ -90,7 +90,7 @@
val before_set2pred_simp_tac =
(simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
-val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
+val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]));
(*****************************************************************************)
(** set2pred_tac transforms sets inclusion into predicates implication, **)
@@ -111,7 +111,7 @@
rtac CollectI i,
dtac CollectD i,
TRY (split_all_tac i) THEN_MAYBE
- (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)]);
+ (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]) i)]);
(*****************************************************************************)
(** BasicSimpTac is called to simplify all verification conditions. It does **)
@@ -125,7 +125,7 @@
fun BasicSimpTac var_names tac =
simp_tac
- (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] addsimprocs [record_simproc])
+ (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc])
THEN_MAYBE' MaxSimpTac var_names tac;