Mon, 20 Aug 2007 17:31:01 +0200 no_document for Infinite_Set, Parity
huffman [Mon, 20 Aug 2007 17:31:01 +0200] rev 24337
no_document for Infinite_Set, Parity
Mon, 20 Aug 2007 11:18:18 +0200 removed allpairs
nipkow [Mon, 20 Aug 2007 11:18:18 +0200] rev 24336
removed allpairs
Mon, 20 Aug 2007 11:18:07 +0200 removed allpairs - use list comprehension!
nipkow [Mon, 20 Aug 2007 11:18:07 +0200] rev 24335
removed allpairs - use list comprehension!
Mon, 20 Aug 2007 04:44:35 +0200 added header
kleing [Mon, 20 Aug 2007 04:44:35 +0200] rev 24334
added header
Mon, 20 Aug 2007 04:34:31 +0200 * HOL-Word:
kleing [Mon, 20 Aug 2007 04:34:31 +0200] rev 24333
* HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution
Mon, 20 Aug 2007 00:22:18 +0200 boolean algebras as locales and numbers as types by Brian Huffman
kleing [Mon, 20 Aug 2007 00:22:18 +0200] rev 24332
boolean algebras as locales and numbers as types by Brian Huffman
Sun, 19 Aug 2007 21:21:37 +0200 Made UN_Un simp
nipkow [Sun, 19 Aug 2007 21:21:37 +0200] rev 24331
Made UN_Un simp
Sun, 19 Aug 2007 12:43:05 +0200 Use 376/377 specials for sendback markup
aspinall [Sun, 19 Aug 2007 12:43:05 +0200] rev 24330
Use 376/377 specials for sendback markup
Sat, 18 Aug 2007 21:27:52 +0200 ML system provides get_print_depth;
wenzelm [Sat, 18 Aug 2007 21:27:52 +0200] rev 24329
ML system provides get_print_depth;
Sat, 18 Aug 2007 19:25:28 +0200 fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
webertj [Sat, 18 Aug 2007 19:25:28 +0200] rev 24328
fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip