--- a/NEWS Tue Sep 06 21:36:48 2016 +0200
+++ b/NEWS Wed Sep 07 22:28:30 2016 +0200
@@ -66,7 +66,15 @@
is relevant to avoid confusion of Pure.simp vs. HOL.simp.
* Commands 'prf' and 'full_prf' are somewhat more informative (again):
-proof terms are reconstructed and cleaned from administrative thm nodes.
+proof terms are reconstructed and cleaned from administrative thm
+nodes.
+
+* The command 'unfolding' and proof method "unfold" include a second
+stage where given equations are passed through the attribute "abs_def"
+before rewriting. This ensures that definitions are fully expanded,
+regardless of the actual parameters that are provided. Rare
+INCOMPATIBILITY in some corner cases: use proof method (simp only:)
+instead, or declare [[unfold_abs_def = false]] in the proof context.
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Isar_Ref/Generic.thy Tue Sep 06 21:36:48 2016 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Wed Sep 07 22:28:30 2016 +0200
@@ -84,6 +84,11 @@
fold back) the given definitions throughout all goals; any chained facts
provided are inserted into the goal and subject to rewriting as well.
+ Unfolding works in two stages: first, the given equations are used directly
+ for rewriting; second, the equations are passed through the attribute
+ @{attribute_ref abs_def} before rewriting --- to ensure that definitions are
+ fully expanded, regardless of the actual parameters that are provided.
+
\<^descr> @{method insert}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> inserts theorems as facts into all goals of
the proof state. Note that current facts indicated for forward chaining are
ignored.
@@ -155,8 +160,8 @@
expand and fold back again the given definitions throughout a rule.
\<^descr> @{attribute abs_def} turns an equation of the form @{prop "f x y \<equiv> t"}
- into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method simp} or @{method
- unfold} steps always expand it. This also works for object-logic equality.
+ into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method simp} steps always
+ expand it. This also works for object-logic equality.
\<^descr> @{attribute rotated}~\<open>n\<close> rotate the premises of a theorem by \<open>n\<close> (default
1).
--- a/src/Doc/Isar_Ref/Proof.thy Tue Sep 06 21:36:48 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Wed Sep 07 22:28:30 2016 +0200
@@ -332,8 +332,8 @@
"proof"}).
\<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command
- "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the
- goal state and facts.
+ "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the goal
+ state and facts. See also the proof method @{method_ref unfold}.
\<^descr> \<^theory_text>\<open>(use b\<^sub>1 \<dots> b\<^sub>n in method)\<close> uses the facts in the given method
expression. The facts provided by the proof state (via @{command "using"}
--- a/src/Pure/Isar/local_defs.ML Tue Sep 06 21:36:48 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML Wed Sep 07 22:28:30 2016 +0200
@@ -207,7 +207,7 @@
(* unfold object-level rules *)
-val unfold_abs_def_raw = Config.declare ("unfold_abs_def", @{here}) (K (Config.Bool false));
+val unfold_abs_def_raw = Config.declare ("unfold_abs_def", @{here}) (K (Config.Bool true));
val unfold_abs_def = Config.bool unfold_abs_def_raw;
local