--- a/NEWS Fri Feb 23 13:09:45 2018 +0100
+++ b/NEWS Fri Feb 23 14:12:48 2018 +0100
@@ -167,6 +167,15 @@
latex and bibtex process. Minor INCOMPATIBILITY.
+*** Isar ***
+
+* Command 'interpret' no longer exposes resulting theorems as literal
+facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
+improves modularity of proofs and scalability of locale interpretation.
+Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
+(e.g. use 'find_theorems' or 'try' to figure this out).
+
+
*** HOL ***
* Clarifed theorem names:
--- a/src/Pure/Isar/interpretation.ML Fri Feb 23 13:09:45 2018 +0100
+++ b/src/Pure/Isar/interpretation.ML Fri Feb 23 14:12:48 2018 +0100
@@ -175,10 +175,14 @@
fun setup_proof after_qed propss eqns goal_ctxt =
Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
propss eqns goal_ctxt state;
+ fun add_registration reg mixin export ctxt = ctxt
+ |> Proof_Context.set_stmt false
+ |> Context.proof_map (Locale.add_registration reg mixin export)
+ |> Proof_Context.restore_stmt ctxt;
in
Proof.context_of state
|> generic_interpretation prep_interpretation setup_proof
- Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns
+ Attrib.local_notes add_registration expression [] raw_eqns
end;
in