changeset 37868 | 59eed00bfd8e |
parent 37820 | ffaca9167c16 |
child 37939 | 965537d86fcc |
--- a/NEWS Wed Jul 21 14:27:05 2010 +0200 +++ b/NEWS Wed Jul 21 15:02:51 2010 +0200 @@ -103,6 +103,15 @@ similar to inductive_cases. +*** ML *** + +* ML antiquotations @{theory} and @{theory_ref} refer to named +theories from the ancestry of the current context, not any accidental +theory loader state as before. Potential INCOMPATIBILITY, subtle +change in semantics. + + + New in Isabelle2009-2 (June 2010) ---------------------------------