# HG changeset patch
# User wenzelm
# Date 1331653206 -3600
# Node ID f30e941b451224dbe3f4e8cb327b51484e6778d9
# Parent  3d44892ac0d64c5b5d003a40f64d1301b1b6e472
prefer abs_def over def_raw;

diff -r 3d44892ac0d6 -r f30e941b4512 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Big_Operators.thy	Tue Mar 13 16:40:06 2012 +0100
@@ -1537,11 +1537,11 @@
 
 lemma dual_max:
   "ord.max (op \<ge>) = min"
-  by (auto simp add: ord.max_def_raw min_def fun_eq_iff)
+  by (auto simp add: ord.max_def min_def fun_eq_iff)
 
 lemma dual_min:
   "ord.min (op \<ge>) = max"
-  by (auto simp add: ord.min_def_raw max_def fun_eq_iff)
+  by (auto simp add: ord.min_def max_def fun_eq_iff)
 
 lemma strict_below_fold1_iff:
   assumes "finite A" and "A \<noteq> {}"
diff -r 3d44892ac0d6 -r f30e941b4512 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Series.thy	Tue Mar 13 16:40:06 2012 +0100
@@ -87,10 +87,13 @@
   by (simp add: sums_def summable_def, blast)
 
 lemma summable_sums:
-  fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}" assumes "summable f" shows "f sums (suminf f)"
+  fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
+  assumes "summable f"
+  shows "f sums (suminf f)"
 proof -
-  from assms guess s unfolding summable_def sums_def_raw .. note s = this
-  then show ?thesis unfolding sums_def_raw suminf_def
+  from assms obtain s where s: "(\<lambda>n. setsum f {0..<n}) ----> s"
+    unfolding summable_def sums_def [abs_def] ..
+  then show ?thesis unfolding sums_def [abs_def] suminf_def
     by (rule theI, auto intro!: tendsto_unique[OF trivial_limit_sequentially])
 qed
 
diff -r 3d44892ac0d6 -r f30e941b4512 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 13 16:40:06 2012 +0100
@@ -476,11 +476,11 @@
     pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
 
 val combinator_table =
-  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
-   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
-   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
-   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
-   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
+  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
+   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
+   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
+   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
+   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
 
 fun uncombine_term thy =
   let
diff -r 3d44892ac0d6 -r f30e941b4512 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Mar 13 16:40:06 2012 +0100
@@ -560,7 +560,7 @@
 val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
 
 (* FIXME: "let_simp" is probably redundant now that we also rewrite with
-  "Let_def_raw". *)
+  "Let_def [abs_def]". *)
 val nnf_ss =
   HOL_basic_ss addsimps nnf_extra_simps
     addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
@@ -574,7 +574,7 @@
 val presimplify =
   rewrite_rule (map safe_mk_meta_eq nnf_simps)
   #> simplify nnf_ss
-  #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
+  #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
 
 fun make_nnf ctxt th = case prems_of th of
     [] => th |> presimplify |> make_nnf1 ctxt
diff -r 3d44892ac0d6 -r f30e941b4512 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Mar 13 16:40:06 2012 +0100
@@ -188,8 +188,6 @@
       in  c_variant_abs_multi (ct, cv::vars)  end
       handle CTERM _ => (ct0, rev vars);
 
-val skolem_def_raw = @{thms skolem_def_raw}
-
 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
@@ -210,8 +208,8 @@
       Drule.list_comb (rhs, frees)
       |> Drule.beta_conv cabs |> Thm.apply cTrueprop
     fun tacf [prem] =
-      rewrite_goals_tac skolem_def_raw
-      THEN rtac ((prem |> rewrite_rule skolem_def_raw)
+      rewrite_goals_tac @{thms skolem_def [abs_def]}
+      THEN rtac ((prem |> rewrite_rule @{thms skolem_def [abs_def]})
                  RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
   in
     Goal.prove_internal [ex_tm] conc tacf
diff -r 3d44892ac0d6 -r f30e941b4512 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 13 16:40:06 2012 +0100
@@ -62,7 +62,7 @@
 fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
   let
     val thy = Proof_Context.theory_of ctxt
-    val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
+    val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
     val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
   in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end