command 'interpret' no longer exposes resulting theorems as literal facts;
authorwenzelm
Fri Feb 23 14:12:48 2018 +0100 (17 months ago)
changeset 677022d9918f5b33c
parent 67701 454dfdaf021d
child 67703 8c4806fe827f
command 'interpret' no longer exposes resulting theorems as literal facts;
NEWS
src/Pure/Isar/interpretation.ML
     1.1 --- a/NEWS	Fri Feb 23 13:09:45 2018 +0100
     1.2 +++ b/NEWS	Fri Feb 23 14:12:48 2018 +0100
     1.3 @@ -167,6 +167,15 @@
     1.4  latex and bibtex process. Minor INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* Command 'interpret' no longer exposes resulting theorems as literal
    1.10 +facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
    1.11 +improves modularity of proofs and scalability of locale interpretation.
    1.12 +Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
    1.13 +(e.g. use 'find_theorems' or 'try' to figure this out).
    1.14 +
    1.15 +
    1.16  *** HOL ***
    1.17  
    1.18  * Clarifed theorem names:
     2.1 --- a/src/Pure/Isar/interpretation.ML	Fri Feb 23 13:09:45 2018 +0100
     2.2 +++ b/src/Pure/Isar/interpretation.ML	Fri Feb 23 14:12:48 2018 +0100
     2.3 @@ -175,10 +175,14 @@
     2.4      fun setup_proof after_qed propss eqns goal_ctxt =
     2.5        Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
     2.6          propss eqns goal_ctxt state;
     2.7 +    fun add_registration reg mixin export ctxt = ctxt
     2.8 +      |> Proof_Context.set_stmt false
     2.9 +      |> Context.proof_map (Locale.add_registration reg mixin export)
    2.10 +      |> Proof_Context.restore_stmt ctxt;
    2.11    in
    2.12      Proof.context_of state
    2.13      |> generic_interpretation prep_interpretation setup_proof
    2.14 -      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns
    2.15 +      Attrib.local_notes add_registration expression [] raw_eqns
    2.16    end;
    2.17  
    2.18  in