2007-08-20 ago kleing boolean algebras as locales and numbers as types by Brian Huffman
2007-08-19 ago nipkow Made UN_Un simp
2007-08-19 ago aspinall Use 376/377 specials for sendback markup
2007-08-18 ago wenzelm ML system provides get_print_depth;
2007-08-18 ago webertj fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
2007-08-18 ago wenzelm removed obsolete ML bindings;
2007-08-18 ago wenzelm converted ex/MT.ML;
2007-08-18 ago wenzelm make HOL-ex earlier;
2007-08-18 ago wenzelm NAMED_CRITICAL;
2007-08-18 ago wenzelm removed stateful init: operations take proper theory argument;
2007-08-18 ago wenzelm removed dead code: const_typargs, num_typargs, init;
2007-08-18 ago wenzelm proper signature;
2007-08-18 ago wenzelm removed obsolete atp_method;
2007-08-18 ago wenzelm export more tactics;
2007-08-18 ago wenzelm renamed ResAtpMethods.setup;
2007-08-18 ago wenzelm added at-poly-5.1-para;
2007-08-17 ago wenzelm added CRITICAL section markup;
2007-08-17 ago wenzelm updated generated file;
2007-08-17 ago wenzelm removed obsolete touch_all_thys;
2007-08-17 ago wenzelm compress: proper check_thy;
2007-08-17 ago wenzelm added encoding spec for jEdit;
2007-08-17 ago wenzelm proper signature;
2007-08-17 ago wenzelm proper signature;
2007-08-17 ago wenzelm turned type_lits into configuration option (with attribute);
2007-08-17 ago nipkow removed set_concat_map and improved set_concat
2007-08-17 ago wenzelm check_deps: ensure that theory is actually present, not just update_time > 1;
2007-08-17 ago haftmann tuned order
2007-08-17 ago haftmann reoriented hook application order
2007-08-17 ago haftmann explicit constants for overloaded definitions
2007-08-17 ago haftmann dropped junk
2007-08-17 ago obua tuned
2007-08-17 ago obua changed floatarith lemmas
2007-08-17 ago wenzelm proper signature for Meson;
2007-08-16 ago wenzelm force: non-critical, but also non-thread-safe (potentially multiple evaluations);
2007-08-16 ago wenzelm removed dead code;
2007-08-16 ago wenzelm improved treatment of global interrupts: Thread.EnableBroadcastInterrupt, redefine ignore/raise_interrupt;
2007-08-16 ago wenzelm removed signal setup from root function to on-entry hook;
2007-08-16 ago wenzelm global state transformation: non-critical, but also non-thread-safe;
2007-08-16 ago haftmann fixed OCaml bug
2007-08-16 ago haftmann fixed codegen setup
2007-08-16 ago haftmann added evaluation examples
2007-08-15 ago wenzelm main: wait_timeout (1 second);
2007-08-15 ago wenzelm tuned comments;
2007-08-15 ago wenzelm added sendback;
2007-08-15 ago paulson combining the relevance filter with res_atp
2007-08-15 ago paulson combining the relevance filter with res_atp
2007-08-15 ago paulson ATP blacklisting is now in theory data, attribute noatp
2007-08-15 ago haftmann added Code_Setup
2007-08-15 ago haftmann fixed OCaml bug
2007-08-15 ago haftmann tuned
2007-08-15 ago haftmann extended
2007-08-15 ago haftmann added Eval_Witness theory
2007-08-15 ago haftmann updated code generator setup
2007-08-15 ago haftmann updated
2007-08-14 ago wenzelm renamed standard_read_XXX to standard_parse_XXX;
2007-08-14 ago wenzelm added implicit type mode (cf. Type.mode);
2007-08-14 ago wenzelm Syntax.global_read_sort;
2007-08-14 ago wenzelm infer_types: depend on Type.mode;
2007-08-14 ago wenzelm type mode: models certification mode (default, syntax, abbrev);
2007-08-14 ago wenzelm replaced certify_typ_syntax/abbrev by certify_typ_mode;