summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 23 Feb 2018 14:12:48 +0100 | |

changeset 67702 | 2d9918f5b33c |

parent 67701 | 454dfdaf021d |

child 67703 | 8c4806fe827f |

command 'interpret' no longer exposes resulting theorems as literal facts;

NEWS | file | annotate | diff | comparison | revisions | |

src/Pure/Isar/interpretation.ML | file | annotate | diff | comparison | revisions |

--- 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