changeset 3982 | 2a903ba8d39e |
parent 3968 | ec138de716d9 |
child 3985 | 173fcf95412f |
--- a/NEWS Fri Oct 24 10:31:31 1997 +0200 +++ b/NEWS Fri Oct 24 11:05:21 1997 +0200 @@ -80,6 +80,8 @@ *** HOL *** +* HOL/Map: new theory of `maps' a la VDM. + * HOL/simplifier: added infix function `addsplits': instead of `<simpset> setloop (split_tac <thms>)' you can simply write `<simpset> addsplits <thms>'