author | nipkow |
Fri, 18 Apr 1997 16:54:52 +0200 | |
changeset 2993 | 9e46778b97ab |
parent 2992 | 395686b418a4 |
child 2994 | 3bb5d1b9c3aa |
--- a/NEWS Fri Apr 18 12:01:12 1997 +0200 +++ b/NEWS Fri Apr 18 16:54:52 1997 +0200 @@ -47,6 +47,9 @@ COULD MAKE EXISTING PROOFS FAIL; in case of problems with old proofs, use unsafe_addss and unsafe_auto_tac +* HOL: patterns in case expressions allow tuple patterns as arguments to +constructors, for example `case x of [] => ... | (x,y,z)#ps => ...' + * HOL: primrec now also works with type nat; * HOL: the constant for negation has been renamed from "not" to "Not" to