ZF typechecking
authorpaulson
Wed Jan 27 16:09:54 1999 +0100 (1999-01-27)
changeset 6155e387d188d0ca
parent 6154 6a00a5baef2b
child 6156 0d52e7cbff29
ZF typechecking
NEWS
     1.1 --- a/NEWS	Wed Jan 27 15:58:22 1999 +0100
     1.2 +++ b/NEWS	Wed Jan 27 16:09:54 1999 +0100
     1.3 @@ -75,6 +75,12 @@
     1.4  * simplification automatically does freeness reasoning for datatype
     1.5    constructors;
     1.6  
     1.7 +* automatic type-inference, with AddTCs command to insert new type-checking
     1.8 +  rules;
     1.9 +
    1.10 +* datatype introduction rules are now added as Safe Introduction rules to
    1.11 +  the claset;
    1.12 +
    1.13  * The syntax "if P then x else y" is now available in addition to if(P,x,y).
    1.14  
    1.15