no_document for Infinite_Set, Parity

removed allpairs

removed allpairs - use list comprehension!

added header

* 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

boolean algebras as locales and numbers as types by Brian Huffman

Made UN_Un simp

Use 376/377 specials for sendback markup

ML system provides get_print_depth;

fixed a bug in demult: -a in (-a * b) is no longer treated as atomic

removed obsolete ML bindings;

converted ex/MT.ML;

make HOL-ex earlier;

NAMED_CRITICAL;

removed stateful init: operations take proper theory argument;

removed dead code: const_typargs, num_typargs, init;

proper signature;

removed obsolete atp_method; ResHolClause.XXX_write_file: theory argument;

export more tactics; ResHolClause.literals_of_term: proper theory argument; removed obsolete ResClause.init, ResHolClause.init;

renamed ResAtpMethods.setup;

added at-poly-5.1-para;

added CRITICAL section markup;

updated generated file;

removed obsolete touch_all_thys;

compress: proper check_thy;

added encoding spec for jEdit;

proper signature;

proper signature; removed unused const_types_of;

turned type_lits into configuration option (with attribute);

removed set_concat_map and improved set_concat

check_deps: ensure that theory is actually present, not just update_time > 1;

tuned order