--- a/NEWS Fri Sep 03 14:22:27 1999 +0200 +++ b/NEWS Fri Sep 03 14:23:15 1999 +0200 @@ -100,6 +100,8 @@ --- > (defconst proofstate-proofstart-regexp "^Level [0-9]+" +* function bind_thms stores lists of theorems (cf. bind_thm); + *** HOL ***