tuned;

tuned;

more robust;

Added tag Isabelle2022-RC1 for changeset 6308eaaa88f1

proper path;

misc updates for Isabelle2022-RC1;

clarified release packaging: naproche-20220910 lacks arm64-linux support (and…

more documentation of 'export_classpath' (session ROOT) and…

merged;

more command-line options;

update for release;

streamlined

less specialized euclidean relation on int

update to Isabelle2022 and Ubuntu 22.04;

more operations: for testing purposes;

proper comment: Phabricator remains on Ubuntu 20.04, which is still required as…

provide naproche-20220910 (inactive);

clarified directory names (e.g. for multi-platform remote execution): avoid…

unused;

tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious…

tuned: prefer Scala Regex operations;

update for release;

tuned whitespace;

tuning and updates for release;

NEWS;

discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should…

merged

some slight polishing in the UTM entry

added congruence rule for forallM of Error-Monad

updated to devel

give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient…

merged

enable show_goal_inst by default: match failure is merely a warning (see…

discontinue fragile operations;

proper context option: change of underlying Options.default will not survive…

updated documentation;

support multiple sessions, with cumulative errors;

support Pretty.unformatted, similar to ML version;

support regex patterns on messages;

tuned signature;

removed odd TODO item (see 3391a493f39a);

tuned signature;

tuned output: more Pretty.item;

clarified failure: warning for logical error, exception for program breakdown;

more robust: capture corner case seen in line 631 of…

clarified output;

print goal instantiation for global qed (and variations);

clarified message channel for 'print_state' (NB: the command was originally for…

updated to postgresql-42.5.0;

clarified goal structure with proper instantiation of main goal, to support…

tool to build Isabelle component for PostgreSQL JDBC;

option "show_states" for more verbosity of batch-builds;

tuned --- avoid warnings;

proper antiquotations;

clarified options, following e.g. "show_consts";

proper antiquotations;

inline markup for Output.state (in contrast to c94bba7906d2): make messages…

clarified modules;

proper Envir.subst operations: env is already normalized, using Envir.norm may…

unused (see 15758fced053);

proper umlauts;

show goal instantiation, notably for 'schematic_goal' command (inactive by…

tuned signature;

tuned signature;

tuned;

tuned;

tuned error message;

merged

tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious…

removed obsolete workaround (see Isabelle/91ee232b4211);

Eliminated the temporary material that was already migrated to the Isabelle…

merge from afp-2021-1

tuned;

merged

regenerate site;

New entry CRYSTALS-Kyber

regenerate site;

added missing history in metadata;

retrieve missing change history in metadata migration tool;

metadata and sitegen for Khovansikii_Theorem

backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726

new email address for Maksym

new entry: Khovanski-Theorem

sitegen for Number_Theoretic_Transform

fixed metadata for Hales_Jewett

new entry Number_Theoretic_Transform

new entry Hales Jewett

adapt to only check ROOT for directories in thys (aftermath of…

updated entry for Universal Turing Machines

merged

adapted to antimono

merged

updated to Isabelle/5ea588440b06

adapted to new mono and strict_mono