2007-08-20 nipkow 2007-08-20 Final mods for list comprehension
2007-08-20 haftmann 2007-08-20 renamed code_gen to export_code
2007-08-20 haftmann 2007-08-20 explizit dependencies
2007-08-20 haftmann 2007-08-20 using canonical instantiation interface
2007-08-20 haftmann 2007-08-20 Sup now explicit parameter of complete_lattice
2007-08-20 haftmann 2007-08-20 turned locales intro classes
2007-08-20 haftmann 2007-08-20 updated keywords
2007-08-20 haftmann 2007-08-20 conciliated Inf/Inf_fin
2007-08-20 wenzelm 2007-08-20 type_check: tuned singleton funs case;
2007-08-20 wenzelm 2007-08-20 theory header: more precise imports;
2007-08-20 huffman 2007-08-20 Word/document/root.tex
2007-08-20 huffman 2007-08-20 new root.tex for HOL-Word
2007-08-20 huffman 2007-08-20 no_document for Infinite_Set, Parity
2007-08-20 nipkow 2007-08-20 removed allpairs
2007-08-20 nipkow 2007-08-20 removed allpairs - use list comprehension!
2007-08-20 kleing 2007-08-20 added header
2007-08-20 kleing 2007-08-20 * 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
2007-08-20 kleing 2007-08-20 boolean algebras as locales and numbers as types by Brian Huffman
2007-08-19 nipkow 2007-08-19 Made UN_Un simp
2007-08-19 aspinall 2007-08-19 Use 376/377 specials for sendback markup
2007-08-18 wenzelm 2007-08-18 ML system provides get_print_depth;
2007-08-18 webertj 2007-08-18 fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
2007-08-18 wenzelm 2007-08-18 removed obsolete ML bindings;
2007-08-18 wenzelm 2007-08-18 converted ex/MT.ML;
2007-08-18 wenzelm 2007-08-18 make HOL-ex earlier;
2007-08-18 wenzelm 2007-08-18 NAMED_CRITICAL;
2007-08-18 wenzelm 2007-08-18 removed stateful init: operations take proper theory argument;
2007-08-18 wenzelm 2007-08-18 removed dead code: const_typargs, num_typargs, init;
2007-08-18 wenzelm 2007-08-18 proper signature;
2007-08-18 wenzelm 2007-08-18 removed obsolete atp_method; ResHolClause.XXX_write_file: theory argument;
2007-08-18 wenzelm 2007-08-18 export more tactics; ResHolClause.literals_of_term: proper theory argument; removed obsolete ResClause.init, ResHolClause.init;
2007-08-18 wenzelm 2007-08-18 renamed ResAtpMethods.setup;
2007-08-18 wenzelm 2007-08-18 added at-poly-5.1-para;
2007-08-17 wenzelm 2007-08-17 added CRITICAL section markup;
2007-08-17 wenzelm 2007-08-17 updated generated file;
2007-08-17 wenzelm 2007-08-17 removed obsolete touch_all_thys;
2007-08-17 wenzelm 2007-08-17 compress: proper check_thy;
2007-08-17 wenzelm 2007-08-17 added encoding spec for jEdit;
2007-08-17 wenzelm 2007-08-17 proper signature;
2007-08-17 wenzelm 2007-08-17 proper signature; removed unused const_types_of;
2007-08-17 wenzelm 2007-08-17 turned type_lits into configuration option (with attribute);
2007-08-17 nipkow 2007-08-17 removed set_concat_map and improved set_concat
2007-08-17 wenzelm 2007-08-17 check_deps: ensure that theory is actually present, not just update_time > 1;
2007-08-17 haftmann 2007-08-17 tuned order
2007-08-17 haftmann 2007-08-17 reoriented hook application order
2007-08-17 haftmann 2007-08-17 explicit constants for overloaded definitions
2007-08-17 haftmann 2007-08-17 dropped junk
2007-08-17 obua 2007-08-17 tuned
2007-08-17 obua 2007-08-17 changed floatarith lemmas
2007-08-17 wenzelm 2007-08-17 proper signature for Meson;
2007-08-16 wenzelm 2007-08-16 force: non-critical, but also non-thread-safe (potentially multiple evaluations);
2007-08-16 wenzelm 2007-08-16 removed dead code;
2007-08-16 wenzelm 2007-08-16 improved treatment of global interrupts: Thread.EnableBroadcastInterrupt, redefine ignore/raise_interrupt;
2007-08-16 wenzelm 2007-08-16 removed signal setup from root function to on-entry hook;
2007-08-16 wenzelm 2007-08-16 global state transformation: non-critical, but also non-thread-safe;
2007-08-16 haftmann 2007-08-16 fixed OCaml bug
2007-08-16 haftmann 2007-08-16 fixed codegen setup
2007-08-16 haftmann 2007-08-16 added evaluation examples
2007-08-15 wenzelm 2007-08-15 main: wait_timeout (1 second);
2007-08-15 wenzelm 2007-08-15 tuned comments;