--- a/src/HOL/Decision_Procs/Polynomial_List.thy Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Mon Jun 28 15:32:17 2010 +0200
@@ -425,7 +425,7 @@
lemma poly_exp_eq_zero:
"(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \<noteq> 0)"
-apply (simp only: fun_eq add: all_simps [symmetric])
+apply (simp only: fun_eq add: HOL.all_simps [symmetric])
apply (rule arg_cong [where f = All])
apply (rule ext)
apply (induct_tac "n")
--- a/src/HOL/Extraction/Euclid.thy Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOL/Extraction/Euclid.thy Mon Jun 28 15:32:17 2010 +0200
@@ -44,7 +44,7 @@
done
lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
- by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
+ by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
lemma not_prime_ex_mk:
assumes n: "Suc 0 < n"
--- a/src/HOL/Library/Univ_Poly.thy Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Mon Jun 28 15:32:17 2010 +0200
@@ -407,7 +407,7 @@
lemma (in idom) poly_exp_eq_zero[simp]:
"(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
-apply (simp only: fun_eq add: all_simps [symmetric])
+apply (simp only: fun_eq add: HOL.all_simps [symmetric])
apply (rule arg_cong [where f = All])
apply (rule ext)
apply (induct n)
--- a/src/HOL/Library/positivstellensatz.ML Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Mon Jun 28 15:32:17 2010 +0200
@@ -228,7 +228,7 @@
val prenex_simps =
map (fn th => th RS sym)
([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @
- @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
+ @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
val real_abs_thms1 = @{lemma
"((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Mon Jun 28 15:32:17 2010 +0200
@@ -86,7 +86,7 @@
"(mkfin (a>>s)) = (a>>(mkfin s))"
-lemmas [simp del] = ex_simps all_simps split_paired_Ex
+lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Mon Jun 28 15:32:17 2010 +0200
@@ -192,7 +192,7 @@
"Traces A == (traces A,asig_of A)"
-lemmas [simp del] = ex_simps all_simps split_paired_Ex
+lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
declare Let_def [simp]
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
--- a/src/HOLCF/ex/Focus_ex.thy Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy Mon Jun 28 15:32:17 2010 +0200
@@ -204,7 +204,7 @@
done
lemma lemma4: "is_g(g) --> def_g(g)"
-apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
+apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
apply (rule impI)
apply (erule exE)