tuned signature;

tuned;

tuned signature;

clarified ML_environment: ML_write_global requires "Isabelle";

clarified signature: do not expose internal operation;

some NEWS (instead of proper documentation);

clarified signature;

simplified markup;

explicit setup of operations: avoid hardwired stuff;

clarified environment: allow "read>write" specification;

tuned;

tuned;

check environment name;

support named ML environments, notably "Isabelle", "SML"; more uniform options ML_read_global, ML_write_global; clarified bootstrap environment;

tuned;

tuned;

clarified signature;

clarified -- prefer new 'ML_export' command;

merged

material on finite maps

more uniform cartouche syntax; more documentation;

more uniform cartouche syntax;

more robust exit: avoid later Consolidate_Execution with handle_raw_edits (cf. 2fd3a6d6ba2e);

tuned message;

clarified message;

actually ensure globally unique counter results (amending a5853334c179);

retain original PolyML.pointerEq;

some modernization of notation

deprecation of ASCII syntax for indexed big operators

tuned

merged

tuned proofs

tuned

simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility

dropped redundant syntax translation rules for big operators

moved lemma from AFP

tuned lemmas

merged

tuned

prefer constructive primitive_part over implicit content_decompose

merged

tuned lemmas

more uniform parameter naming convention for choose and gchoose

slightly generalized theorems

tuned code setup

tuned

more theorems on fact

removed ineffective code equation

tuned whitespace

new simp rule

copied but not adapted

improved sectioning

merged

avoid session qualification because no tex is generated when used; tuned sectioning

removed ineffective code declarations

proper code abbreviation for power on real

tuned

tuned

suppress redundant messages;

optional notification of nodes_status (via progress); more accurate changed.nodes wrt. dep_theories; tuned signature;

tuned signature;

tuned;

tuned;

tuned signature;

tuned output;

clarified signature;

clarified signature;

clarified signature;

trim nodes_status: avoid potential memory leak;

simplified (cf. dcd69422b953);

clarified modules;

clarified modules;

Finite_Map: monotonicity

State_Monad: more simp lemmas

enforce ML_system_64: more robust as cold build, without command_timings;

clarified signature;

removed obsolete RC tags;

(re)moved lemmas

updated to renaming

updated common hosts;

merged

Added tag Isabelle2018 for changeset 91162dd89571

merged

canonical session directories in correspondence to Known.files;

Zorn's lemma for relations defined by predicates

merged

proper session dirs;

tuned signature;

tuned;

merged;

Added tag Isabelle2018-RC4 for changeset 34b8ff7cb109

updated for release;

updated screenshot;

updated documentation;

suppress verit-2016post -- not ready for release;

isabelle build options -c -x -B refer to imports_graph;

more uniform checks;

tuned signature;

tuned signature;

tuned signature;

clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;

tuned signature;

export shyps as regular typargs;

more uniform facts: single vs. multi;

explicit names for bound variables;

export in foundational order;

recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;

more Pure theory content;

Small lemmas about analysis

merged

de-applying

tuned output;

tuned signature -- removed somewhat pointless operation;

more operations;

more operations (as in ML);

more explicit entity kind;

Pure theory content;

tuned signature: more operations;

tuned signature;

always export Pure theory;

de-applying

de-applying

de-applying and removal of obsolete aliases

merged

Added tag Isabelle2018-RC3 for changeset 71aa5a9128c2

proper return code (true) if file is absent;

clarified word syntax for the sake of control symbols, e.g. \<^term>;

updated to Poly/ML fixes-5.7.1 b3d1ff33a4b4;

more robust: do not defer potentially slow/big lazy facts to the very end;

more robust: potentially a workaround for spurious HOL build problems seen by Larry Paulson;

tuned;

eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;

unused;

removed junk;

clarified documentation;

added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);

proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises";

proper maxidx: if x does not occur in A, its maxidx could get lost;

tuned;

more flexible session selection as in "isabelle jedit";

updated to jdk-8u181;

merged

de-applying and simplification

datatype_record produces simp theorems; contributed in part by Yu Zhang

updated to jdk-8u181;

de-applying

back to post-release mode -- after fork point;

Added tag Isabelle2018-RC2 for changeset 14167c321d22

tuned;

eliminated spurious Unicode;

merged

updated to kodkodi-1.5.2-1: modernized settings and renamed directory (same executables);

Moved Real_Asymp manual

merged

updated to polyml-5.7.1-7 (see also afa7c5a239e6);

merged

de-applying

avoid Unicode conflict with \<pounds>;

fixing a theorem statement, etc.

merged

de-applying and removing junk

don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)

add lemmas about prod_filter

merged

corrections to markup

updated material concerning Algebra

merged

de-applying

added system option "strict_facts";

slightly more canonical imports

setup for Haskell taken over from AFP / Gauss_Jordan

tuned equation

restructured for future incorporation of Haskell

slightly more uniform style

taken over from AFP / Gauss_Jordan

more cartouches

merged

normalize imports

tagged

evade odd connection problems to https://isabelle.in.tum.de from some remote hosts;

prefer HTTPS;

more ANNOUNCE;

tuned;

more de-applying

merged

de-applying and simplifying proofs

Tagged some more files in HOL-Analysis

Made simproc for sqrt/root of numeral more robust

merged

merged

more examples for Code_Lazy

de-applying and meta-quantifying

merged

more renaming fixes

fixes and more de-applying

more de-applying and a fix

merged

last bit of renaming

de-applying

Added Real_Asymp package

Tagged Conformal_Mappings in HOL-Analysis

merged

merged

de-applying

HOL-Analysis: Volume of a simplex, Heron's theorem

Tagged Ball_Volume and Gamma_Function in HOL-Analysis

correct import

merged

unit_cube = cbox 0 One

relaxed assumptions for dim_image_eq and dim_image_le

merged

de-applying (mostly Set_Interval)

more economic tagging

de-applying (mostly Quotient)

de-applying

more de-applying

patched a continuity proof

merged

de-applying, etc.

moved lemmas

merged

final removal of smt from Algebra

make theorem, corollary, and proposition %important for HOL-Analysis manual

removal of smt and certain refinements

removal of smt

elimination of some "smt"

De-applying

merged

de-applying, etc.

more symmetric

prefer HTTPS;

just one global lock for group status: avoid proliferation of mutexes, condvars;

more frugal assignment of lazy value: fewer mutexes, condvars; cannot use RunCall.clearMutableBit due to spurious crashes;

replaced subgroup_imp_subset in Modules

merged

de-applying

merged

submodules

more manual tests;

store immutable result: fewer refs, mutexes, condvars;