NEWS
changeset 54049 566b769c3477
parent 54033 955c6549b3cb
child 54055 5bf55a713232
child 54305 d2def195bb6b
equal deleted inserted replaced
54048:f6bd38fb2c39 54049:566b769c3477
   101 plugin, which is now enabled by default.
   101 plugin, which is now enabled by default.
   102 
   102 
   103 
   103 
   104 *** Pure ***
   104 *** Pure ***
   105 
   105 
   106 * Target-sensitive commands 'interpretation' and 'sublocale'.
   106 * Commands 'interpretation' and 'sublocale' are now target-sensitive.
   107 Particularly, 'interpretation' now allows for non-persistent
   107 In particular, 'interpretation' allows for non-persistent
   108 interpretation within "context ... begin ... end" blocks.  See
   108 interpretation within "context ... begin ... end" blocks offering a
   109 "isar-ref" manual for details.
   109 light-weight alternative to 'sublocale'.  See "isar-ref" manual for
       
   110 details.
   110 
   111 
   111 * Improved locales diagnostic command 'print_dependencies'.
   112 * Improved locales diagnostic command 'print_dependencies'.
   112 
   113 
   113 * Discontinued obsolete 'axioms' command, which has been marked as
   114 * Discontinued obsolete 'axioms' command, which has been marked as
   114 legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
   115 legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'