NEWS
changeset 67702 2d9918f5b33c
parent 67616 1d005f514417
child 67718 17874d43d3b3
     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: