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

explicit constants for overloaded definitions

dropped junk

tuned

changed floatarith lemmas

proper signature for Meson;

force: non-critical, but also non-thread-safe (potentially multiple evaluations);

removed dead code;

improved treatment of global interrupts: Thread.EnableBroadcastInterrupt, redefine ignore/raise_interrupt;

removed signal setup from root function to on-entry hook;

global state transformation: non-critical, but also non-thread-safe;

fixed OCaml bug

fixed codegen setup

added evaluation examples

main: wait_timeout (1 second);

tuned comments;

added sendback;

combining the relevance filter with res_atp

combining the relevance filter with res_atp

ATP blacklisting is now in theory data, attribute noatp

added Code_Setup

fixed OCaml bug

tuned

extended

added Eval_Witness theory

updated code generator setup

updated

renamed standard_read_XXX to standard_parse_XXX; added global_read/parse_XXX;

added implicit type mode (cf. Type.mode); added inner syntax parsers for sort/typ (no term/prop yet); infer_types: exception TYPE => error; read_vars: Syntax.parse_typ;

Syntax.global_read_sort;

infer_types: depend on Type.mode;

type mode: models certification mode (default, syntax, abbrev); replaced certify_typ_syntax/abbrev by certify_typ_mode;

replaced certify_typ_syntax/abbrev by certify_typ_mode; removed obsolete read_sort', read_typ', read_typ_syntax', read_typ_abbrev';

tuned order;

avoid low-level tsig;

fixed dummyT (used as constraint);

remove redundant assumption from Rep_range lemma

minimize imports

rename lemmas finite->finite_UNIV, finite_set->finite; declare finite[simp]

extended linear arith capabilities with code by Amine

fix the generation of eqvt lemma of equality form from the imp form when the relation is equality

moved Tools/xml.ML to General/xml.ML (again);

added generic wrapper for parse/read functions; renamed read_term to standard_read_term etc.;

tuned;

PrimitiveDefs.dest/abs_def;

PrimitiveDefs.dest_def; Syntax.standard_read;

Primitive definition forms.

moved support for primitive defs to primitive_defs.ML;

use logic.ML earlier; added primitive_defs.ML;

moved Tools/xml.ML to General/xml.ML (again); added primitive_defs.ML;

PrimitiveDefs.mk_defpair;

be a bit more ressource cautious with multi-threading (-M 20 instead of 99)

fixed syntax

simplified

fixed OCaml bug

*** empty log message ***

renamed keyword "to" to "module_name"

dropped code_axioms

moved appl syntax to PureThy; structure Lexicon: not hidden;

Lexicon.tokenize: do not appen EndToken yet; term: include var, &&;

Lexicon.tokenize: do not appen EndToken yet;

Lexicon.read_indexname/nat/variable;

moved appl syntax to PureThy; SimpleSyntax.read_typ/term/prop;

moved appl syntax to PureThy;

SimpleSyntax.read_prop;

added atbroy9