--- 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> {}"
--- 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
--- 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
--- 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
--- 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
--- 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