diff -r 02e9b54b18fd -r 8b26f58c5646 NEWS --- a/NEWS Tue Sep 19 23:12:21 2006 +0200 +++ b/NEWS Tue Sep 19 23:15:24 2006 +0200 @@ -465,6 +465,9 @@ * Pure: 'class_deps' command visualizes the subclass relation, using the graph browser tool. +* Pure: 'print_theory' now suppresses entities with internal name +(trailing "_") by default; use '!' option for full details. + *** HOL ***