haftmann [Mon, 20 Aug 2007 18:07:28 +0200] rev 24344
turned locales intro classes
haftmann [Mon, 20 Aug 2007 18:07:26 +0200] rev 24343
updated keywords
haftmann [Mon, 20 Aug 2007 18:07:25 +0200] rev 24342
conciliated Inf/Inf_fin
wenzelm [Mon, 20 Aug 2007 17:46:32 +0200] rev 24341
type_check: tuned singleton funs case;
wenzelm [Mon, 20 Aug 2007 17:46:31 +0200] rev 24340
theory header: more precise imports;
huffman [Mon, 20 Aug 2007 17:34:04 +0200] rev 24339
Word/document/root.tex
huffman [Mon, 20 Aug 2007 17:31:59 +0200] rev 24338
new root.tex for HOL-Word
huffman [Mon, 20 Aug 2007 17:31:01 +0200] rev 24337
no_document for Infinite_Set, Parity
nipkow [Mon, 20 Aug 2007 11:18:18 +0200] rev 24336
removed allpairs
nipkow [Mon, 20 Aug 2007 11:18:07 +0200] rev 24335
removed allpairs - use list comprehension!
kleing [Mon, 20 Aug 2007 04:44:35 +0200] rev 24334
added header
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
kleing [Mon, 20 Aug 2007 00:22:18 +0200] rev 24332
boolean algebras as locales and numbers as types by Brian Huffman
nipkow [Sun, 19 Aug 2007 21:21:37 +0200] rev 24331
Made UN_Un simp
aspinall [Sun, 19 Aug 2007 12:43:05 +0200] rev 24330
Use 376/377 specials for sendback markup
wenzelm [Sat, 18 Aug 2007 21:27:52 +0200] rev 24329
ML system provides get_print_depth;
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
wenzelm [Sat, 18 Aug 2007 17:42:39 +0200] rev 24327
removed obsolete ML bindings;
wenzelm [Sat, 18 Aug 2007 17:42:38 +0200] rev 24326
converted ex/MT.ML;
wenzelm [Sat, 18 Aug 2007 13:32:28 +0200] rev 24325
make HOL-ex earlier;
wenzelm [Sat, 18 Aug 2007 13:32:26 +0200] rev 24324
NAMED_CRITICAL;
wenzelm [Sat, 18 Aug 2007 13:32:25 +0200] rev 24323
removed stateful init: operations take proper theory argument;
wenzelm [Sat, 18 Aug 2007 13:32:23 +0200] rev 24322
removed dead code: const_typargs, num_typargs, init;
wenzelm [Sat, 18 Aug 2007 13:32:22 +0200] rev 24321
proper signature;
wenzelm [Sat, 18 Aug 2007 13:32:21 +0200] rev 24320
removed obsolete atp_method;
ResHolClause.XXX_write_file: theory argument;
wenzelm [Sat, 18 Aug 2007 13:32:20 +0200] rev 24319
export more tactics;
ResHolClause.literals_of_term: proper theory argument;
removed obsolete ResClause.init, ResHolClause.init;
wenzelm [Sat, 18 Aug 2007 13:32:18 +0200] rev 24318
renamed ResAtpMethods.setup;
wenzelm [Sat, 18 Aug 2007 00:22:22 +0200] rev 24317
added at-poly-5.1-para;