# HG changeset patch
# User haftmann
# Date 1277731937 -7200
# Node ID 893dcabf0c0486f44c7b91616b1876d926726e3e
# Parent  a02ea93e88c6a3944beb49b3384cd031782e9897
explicit is better than implicit

diff -r a02ea93e88c6 -r 893dcabf0c04 src/HOL/Decision_Procs/Polynomial_List.thy
--- 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")
diff -r a02ea93e88c6 -r 893dcabf0c04 src/HOL/Extraction/Euclid.thy
--- 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"
diff -r a02ea93e88c6 -r 893dcabf0c04 src/HOL/Library/Univ_Poly.thy
--- 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)
diff -r a02ea93e88c6 -r 893dcabf0c04 src/HOL/Library/positivstellensatz.ML
--- 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
diff -r a02ea93e88c6 -r 893dcabf0c04 src/HOLCF/IOA/meta_theory/TLS.thy
--- 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") *}
 
diff -r a02ea93e88c6 -r 893dcabf0c04 src/HOLCF/IOA/meta_theory/Traces.thy
--- 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") *}
 
diff -r a02ea93e88c6 -r 893dcabf0c04 src/HOLCF/ex/Focus_ex.thy
--- 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)