reorganize into subsections

prepare_dummies: NAMED_CRITICAL;

with_modes []: non-critical;

tuned signature;

File.read/write/append: non-critical (basic IO operations already thread-safe);

TextIO.inputLine: non-critical (assume exclusive ownership);

tuned merge operations via pointer_eq;

cleaned up; declared more simp rules

issue a warning, when encountering redundant equations (covered by prece3ding clauses)

remove int_of_nat

remove int_of_nat; fix abs instance

use overloaded bitwise operators at type int

use class instead of axclass

theory header: fixed import;

headers for document generation

Final mods for list comprehension

renamed code_gen to export_code

explizit dependencies

using canonical instantiation interface

Sup now explicit parameter of complete_lattice

turned locales intro classes

updated keywords

conciliated Inf/Inf_fin

type_check: tuned singleton funs case;

theory header: more precise imports;

Word/document/root.tex

new root.tex for HOL-Word

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

reoriented hook application order