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

multi-threading with poly 5.1 test

new attribute [rotated]

tuned comments;

Simple syntax for types and terms --- for bootstrapping Pure.

added Syntax/simple_syntax.ML;

* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;

read_def_terms': restrict scope of disambiguation to individual term;

stream source: non-critical, assuming exclusive ownership;

added type constraints to resolve syntax ambiguities;

made SML/NJ happy;

schedule_tasks: alphabetical order for equivalent tasks;

simultaneous use_thys;

tuned ML bindings;

tuned

dropped code generator setup garbage

syntax fix

corrected code generator module names

new structure for code generator modules

code generator setup improved