words added to code generator test

a generic horner sum operation

more thms

clarified message --- as in former ML version (see 940195fbb282);

clarified signature;

clarified messages: avoid duplicate Timing;

clarified messages;

clarified signature;

tuned;

avoid duplicate Timing messages (see also 5c4800f6b25a);

more accurate message;

tuned;

clarified signature;

clarified inlined protocol messages;

removed unused property;

signed_take_bit

more on single-bit operations

proper session Timing for build_history log file (see 5c4800f6b25a);

clarified signature;

more robust, notably for isabelle_cronjob;

more robust build_session protocol: allow prover process to terminate/crash without build_session_finished message;

Update Metis to 2.4

updated to polyml-5.8.1-20200708: recent repository version for testing;

more robust protocol for "Timing ..." messages, notably for pide_session=true;

removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible with post-2016 reforms to local theories

separation of traditional bit operations

no pide_session on macos: avoid odd "hang" of remote_build_history;

support generated preferences, i.e. non-strict system options;

factored out auxiliary theory

prefer explicit proof

tuned whitespace;

use less memory on old hardware;

clarified signature;

clarified log message (more uniform);

misc lemma tuning

explicit proofs for bit projections

extraction of equations x = t from premises beneath meta-all

a small aggiornamento for Z2

removed superfluous dependency

factored out ancient numeral representation

moved to Word_Lib

more explicit proofs

clarified options --- potentially more robust;

tuned message;

clarified signature;

more CONTRIBUTORS;

more uniform URL (see 60b5a4731695);

clarified use of memory: prefer share tree structures over fresh strings;

more Java heap space (see 2d658beb815b);

clarified NEWS;

enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);

discontinued old AFP test: ancient hardware with insufficient resources;

tuned output;

merged

share cache for parallel sessions;

clarified signature;

more caching, notably for build/pide_session;

removed pointless pide_exports: unused during "build_session" process (reverting 6a64205b491a);

tuned --- avoid error in IntelliJ IDEA;

simp rules for conversions

more class operations for the sake of efficient generated code

merged

back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);

back to pide_session=false for now, requires too many JVM resources (reverting 026de3424c39);

clarified signature;

avoid redundant export handling for build;

prefer single name

more lemmas

build bit operations on word on library theory on bit operations

bit operations as distinctive library theory

tweak for code generation

pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all

more lemmas and less name space pollution

canonical bit shifts for word type, leaving duplicates as they are at the moment

essential instance about bit structure

more transfer rules

dropped yet another duplicate

fundamental construction of word type following existing transfer rules

replaced mere alias by input abbreviation

replaced mere alias by abbreviation

replaced operation with weak abstraction by input abbreviation

avoid compound operation

formal relationships between operations

eliminated warnings

replaced mere alias by input abbreviation

enable pide_session by default;

avoid resource problems of JVM by too many parallel XZ compression tasks;

interpretations for boolean operators

more specific thm reference

clarified errors;

fixed the utterly weird definitions of asym / asymp, and added many asym lemmas

tuned whitespace;

proper rendering of complex codepoints, e.g. \<^url> code: 0x01F310;

updated to jedit-5.6pre1 (repository version 25349);

simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)

New Ackermann development

tuned document;

proper latex macros, notably for src/HOL/Examples/Iff_Oracle.thy;

NEWS;

clarified sessions;

clarified sessions: "Notable Examples in Isabelle/HOL";

clarified sessions: "Notable Examples in Isabelle/Pure";

NEWS

more theorems

avoid overaggressive default simp rules

activate simproc for FOL

more rules for FOL also

more simp rules

should have been copied across from Set.thy as well for better printing

specific atomization inert to later rule set modifications

more precise scope of atomize

install simproc but deactivate by default

adapted to d25093536482;

clarified markup;

clarified signature;

tuned signature;

tuned;

more NEWS;

more documentation on Isabelle/Scala;

proper error positions;