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;

tuned;

tuned whitespace;

more antiquotations;

check bash functions against Isabelle settings environment;

misc tuning;

breakable scala_name;

tuned signature;

discontinued pointless document antiquotation;

proper check of example;

clarified signature --- fit within limit of 22 arguments;

tuned;

tuned;

more antiquotations;

obsolete;

check free-form Scala source;

clarified static_check: avoid accidental evaluation;

omit pointless memoing: Scala compiler is rather bulky anyway;

clarified signature;

antiquotations for Scala entities;

better closeup and more consistent terminology

merged

proper stack_limit;

clarified signature;

more accurate classpath for "isabelle scala";

proper check of registered Scala functions;

asynchronous build_session: notably for Scala.fulfill protocol commands during run;

clarified build_session protocol;

clarified signature;

clarified name;

more robust: explicit check for PIDE session;

tuned signature;

unused;

tuned signature;

check Scala source snippets from ML;

more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;

init default context;

tuned message;

clarified signature;

tuned;

more brackets (see 2e8af171887f);

tuned message;

clarified signature; more operations;

unused;

more robust, notably for "isabelle scala";

clarified signature;

reorganised sorted_set_of_list

merged

simpler inductions

a few new lemmas about functions

comment makes no sense

added simp lemma

slightly more specific implementations

tuned module name space for generated code

unused alias

generalized and augmented

clarified signature;

clarified modules;

A few new theorems, plus some tidying up

corrected spelling and tuned whitespace

tuned

follow Phabricator update 2020 Week 19;

another AVL tree version

added missing preprocessing step for extraction (due to Stefan Berghofer)

new HOL simproc: eliminate_false_implies

added lemma

Tuned some proofs in HOL-Analysis

The Uniq quantifier for FOL too

generalised pigeonhole principle in HOL-Library.FuncSet

new constant power_int in HOL

New HOL simproc 'datatype_no_proper_subterm'

merged

Fixes for Sup{} = (0::nat)

abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)

clarified session imports: avoid bulky HOL-Library image;

tuned -- avoid warning;

"app" -> "join" for RBTs

"app" -> "join" for uniformity with Join theory; tuned defs

added top-level functions and tuned

the Uniq quantifier

modernized notation for bit operations

merged

avoid hidden undef cases

explicit mask operation for bits

prefer _ mod 2 over of_bool (odd _)

less aggressive default simp rules

simplified and tuned

tuned

tuned

tuned proofs

tuned var. names

tuned var. names

AVL trees with balance tags

A little more tidying up

tuned

merged

tuned

merged

added "isabelle sessions" tool;

tuned messages;

use abs(h l - h r) instead of 3 cases, tuned proofs

added lemmas

simplified construction of binary bit operations

temporarily revert change which does not work as expected

more rules

added Height_Balanced_Trees

documentation of relevant ideas

numeral rules for take_bit / drop_bit on int

opaque export does not work as expected in presence of dependent instances

merged

tuned document

split AVL_Set.thy

avoid passing chained facts twice to preplay in Sledgehammer

tweaked Vampire's options + tuning

more robust Isabelle_System.init (amending c0bc99aad936): avoid non-termination on Windows (java.lang.StackOverflowError);

back to more modest (but uniform) Java stack, see 97fc4f657bda;

more generous Java memory, also hoping to prevent spurious java.lang.StackOverflowError in isabelle_cronjob;

added lemmas

hooks for foundational terms: protection of foundational terms during simplification

merged

merged

avoid deprecated operations;

tuned -- avoid odd compiler warning;

avoid deprecated operations;

deprecated and obsolete;

tuned signature -- avoid warnings;

more informative error;

new funs successive and distinct_adj

added lemmas

clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;

clarified signature -- avoid warning;

tuned;

clarified imports;

more robust judgment handling

Sketch and explore again

removal of symmetries in Polytope, plus some tidying

Sketch_and_Explore — oops

the rest of the applys

more applys

merged

New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists

discontinued somewhat incoherent patches (see also 3b36fc4916af);

use friendlier package;

removed LaTeX package and hack to avoid ALLCAPS headers

use friendlier package

move virtual machine node;

generalized

more theorems

another rule on numerals

bit on numerals

more complete rules on numerals

more complete rules on numerals

removed obsolete RC tags;

merged

Added tag Isabelle2020 for changeset abf3e80bd815

tuned NEWS;

tuned NEWS;

tuned message; tuned signature;

tuned message;

clarified signature;

more cleaning up Homotopy

cleaning up Homotopy

merged

more removal of applys

avoid hard-wired stuff: configure via plugin services;

tuned;

tuned;