adapted to Isabelle 80d7f004089d

Heptapod acknowledgements

new entry: Safe_Distance

website for Safe_Distance

added missing HTML file

new entry Nash_Williams

sitegen for Nash_Williams

metadata and sitegen for Smith-Normal-Form

new entry: Smith normal form

changed import to prepare for Smith-Normal-Form submission

new entries

more uniform URL (see 60b5a4731695);

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

more Java heap space (see 2d658beb815b);

Merge branch 'master' of github.com:dcjm/polyml

Posix.FileSys.wordToFD should always make persistent file descriptors i.e. they…

clarified NEWS;

enable pide_session by default (again), with extra JVM heap for AFP tests (see…

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…

tuned --- avoid error in IntelliJ IDEA;

simp rules for conversions

more class operations for the sake of efficient generated code

more class operations for the sake of efficient generated code

merged

back to parallel compression: full AFP build does require 16GB Java heap…

back to pide_session=false for now, requires too many JVM resources (reverting…

clarified signature;

avoid redundant export handling for build;

prefer single name

prefer single name

Fix the transformation that chains SetContainers. This was changed as a result…

When loading a container address use native-word rather than poly-word.

When loading from the stack always load a native word, i.e. 64-bits in 32-in-64.

build bit operations on word on library theory on bit operations

more instances for uint types

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

dropped yet another duplicate

replaced mere alias by input abbreviation

replaced mere alias by abbreviation

replaced operation with weak abstraction by input abbreviation

avoid compound operation

replaced mere alias by input abbreviation

more lemmas

bit operations as distinctive library theory

build bit operations on word on library theory on bit operations

tweak for code generation

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

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

fundamental construction of word type following existing transfer rules

dropped yet another duplicate

replaced mere alias by input abbreviation

replaced operation with weak abstraction by input abbreviation

replaced mere alias by 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;

eliminated needless locale

more renamings in Saturation Framework

renamed locales as discussed with Sophie Tourret

added file that was part of previous renaming/refactoring

renamed file in Saturation_Framework following discussion with Sophie Tourret

interpretations for boolean operators

more specific thm reference

interpretations for boolean operators

Tweak completeness proof

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);

proper file;

stronger * with + cancellation lemmas

simplified 'smt_proofs' option to be a binary option (instead of ternary), now…

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";

Invalid constant indexes for arrays or vectors can result in an overflow when…

NEWS

more theorems

avoid overaggressive default simp rules