| changeset 32433 | 11661f4327bb |
| parent 32427 | 0a94e1f264ce |
| child 32463 | 3a0a65ca2261 |
--- a/NEWS Fri Aug 28 21:04:03 2009 +0200 +++ b/NEWS Fri Aug 28 21:15:22 2009 +0200 @@ -181,6 +181,10 @@ or even Display.pretty_thm_without_context as last resort. INCOMPATIBILITY. +* Discontinued Display.pretty_ctyp/cterm etc. INCOMPATIBILITY, use +Syntax.pretty_typ/term directly, preferably with proper context +instead of global theory. + *** System ***