ZF: division
authorpaulson
Mon, 21 May 2001 12:51:15 +0200
changeset 11314 f6eebbbed449
parent 11313 04c8da2e0917
child 11315 fbca0f74bcef
ZF: division
NEWS
--- a/NEWS	Sun May 20 13:16:27 2001 +0200
+++ b/NEWS	Mon May 21 12:51:15 2001 +0200
@@ -14,6 +14,9 @@
   (rare) case use   delSWrapper "split_all_tac" addSbefore 
                     ("unsafe_split_all_tac", unsafe_split_all_tac)
 
+* ZF: the integer library now covers quotients and remainders, with many laws
+relating division to addition, multiplication, etc.;
+
 
 New in Isabelle99-2 (February 2001)
 -----------------------------------