explicit is better than implicit
authorhaftmann
Mon Jun 28 15:32:17 2010 +0200 (2010-06-28)
changeset 37598893dcabf0c04
parent 37597 a02ea93e88c6
child 37599 b8e3400dab19
explicit is better than implicit
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Extraction/Euclid.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Library/positivstellensatz.ML
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.thy
src/HOLCF/ex/Focus_ex.thy
     1.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Jun 28 15:32:13 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Jun 28 15:32:17 2010 +0200
     1.3 @@ -425,7 +425,7 @@
     1.4  
     1.5  lemma poly_exp_eq_zero:
     1.6       "(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \<noteq> 0)"
     1.7 -apply (simp only: fun_eq add: all_simps [symmetric]) 
     1.8 +apply (simp only: fun_eq add: HOL.all_simps [symmetric]) 
     1.9  apply (rule arg_cong [where f = All]) 
    1.10  apply (rule ext)
    1.11  apply (induct_tac "n")
     2.1 --- a/src/HOL/Extraction/Euclid.thy	Mon Jun 28 15:32:13 2010 +0200
     2.2 +++ b/src/HOL/Extraction/Euclid.thy	Mon Jun 28 15:32:17 2010 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4    done
     2.5  
     2.6  lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
     2.7 -  by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
     2.8 +  by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
     2.9  
    2.10  lemma not_prime_ex_mk:
    2.11    assumes n: "Suc 0 < n"
     3.1 --- a/src/HOL/Library/Univ_Poly.thy	Mon Jun 28 15:32:13 2010 +0200
     3.2 +++ b/src/HOL/Library/Univ_Poly.thy	Mon Jun 28 15:32:17 2010 +0200
     3.3 @@ -407,7 +407,7 @@
     3.4  
     3.5  lemma (in idom) poly_exp_eq_zero[simp]:
     3.6       "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
     3.7 -apply (simp only: fun_eq add: all_simps [symmetric])
     3.8 +apply (simp only: fun_eq add: HOL.all_simps [symmetric])
     3.9  apply (rule arg_cong [where f = All])
    3.10  apply (rule ext)
    3.11  apply (induct n)
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Jun 28 15:32:13 2010 +0200
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Jun 28 15:32:17 2010 +0200
     4.3 @@ -228,7 +228,7 @@
     4.4  val prenex_simps =
     4.5    map (fn th => th RS sym)
     4.6      ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @
     4.7 -      @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
     4.8 +      @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
     4.9  
    4.10  val real_abs_thms1 = @{lemma
    4.11    "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and
     5.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Jun 28 15:32:13 2010 +0200
     5.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Mon Jun 28 15:32:17 2010 +0200
     5.3 @@ -86,7 +86,7 @@
     5.4    "(mkfin (a>>s)) = (a>>(mkfin s))"
     5.5  
     5.6  
     5.7 -lemmas [simp del] = ex_simps all_simps split_paired_Ex
     5.8 +lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
     5.9  
    5.10  declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
    5.11  
     6.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Mon Jun 28 15:32:13 2010 +0200
     6.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Mon Jun 28 15:32:17 2010 +0200
     6.3 @@ -192,7 +192,7 @@
     6.4    "Traces A == (traces A,asig_of A)"
     6.5  
     6.6  
     6.7 -lemmas [simp del] = ex_simps all_simps split_paired_Ex
     6.8 +lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
     6.9  declare Let_def [simp]
    6.10  declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
    6.11  
     7.1 --- a/src/HOLCF/ex/Focus_ex.thy	Mon Jun 28 15:32:13 2010 +0200
     7.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Mon Jun 28 15:32:17 2010 +0200
     7.3 @@ -204,7 +204,7 @@
     7.4  done
     7.5  
     7.6  lemma lemma4: "is_g(g) --> def_g(g)"
     7.7 -apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
     7.8 +apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
     7.9    addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
    7.10  apply (rule impI)
    7.11  apply (erule exE)