3 months ago wenzelm 2019-07-20 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
3 months ago wenzelm 2019-07-20 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
3 months ago wenzelm 2019-07-20 more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
3 months ago paulson 2019-07-19 More results about measure and integration theory
3 months ago paulson 2019-07-18 More analysis / measure theory material
3 months ago paulson 2019-07-18 merged
3 months ago paulson 2019-07-18 more new material about analysis
3 months ago nipkow 2019-07-18 added forgotten declaration provided by Florian Haftmann
3 months ago wenzelm 2019-07-17 merged;
3 months ago wenzelm 2019-07-17 updated to jedit_build-20190717: support more brackets;
3 months ago wenzelm 2019-07-17 updated to isabelle_fonts-20190717;
3 months ago wenzelm 2019-07-17 redundant;
3 months ago wenzelm 2019-07-17 tuned;
3 months ago wenzelm 2019-07-17 added \<llangle>, \<rrangle>; discontinued special rendering for old {* *};
3 months ago wenzelm 2019-07-17 tuned doc isar-ref;
3 months ago wenzelm 2019-07-17 added \<bbar>;
3 months ago wenzelm 2019-07-17 added \<sqdot>;
3 months ago paulson 2019-07-17 fixed renaming issues
3 months ago paulson 2019-07-17 merged
3 months ago paulson 2019-07-17 a few new lemmas and a bit of tidying
4 months ago wenzelm 2019-07-16 support for a soft-type system within the Isabelle logical framework;
4 months ago nipkow 2019-07-11 tuned
4 months ago wenzelm 2019-07-04 proper theory naming after join (reset due to merge_data);
4 months ago wenzelm 2019-07-04 support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
4 months ago wenzelm 2019-07-04 clarified history stage: allow independent updates that are merged later;
4 months ago wenzelm 2019-06-24 support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);
4 months ago haftmann 2019-06-23 proper quasi-total merge
4 months ago haftmann 2019-06-22 made LaTeX happy
4 months ago haftmann 2019-06-22 streamlined setup for linear algebra, particularly removed redundant rule declarations
4 months ago haftmann 2019-06-22 tuned
4 months ago haftmann 2019-06-21 tuned
5 months ago haftmann 2019-06-16 even more appropriate fact name
5 months ago haftmann 2019-06-16 more correct indicator
5 months ago haftmann 2019-06-14 make latex happy
5 months ago haftmann 2019-06-14 moved some theorems into HOL main corpus
5 months ago haftmann 2019-06-14 misc tuning and modernization
5 months ago haftmann 2019-06-14 more theorems for proof of concept for word type
5 months ago haftmann 2019-06-14 official fact collection sign_simps
5 months ago haftmann 2019-06-14 tuned proofs
5 months ago haftmann 2019-06-14 avoid pseudo-collection to be used in generated proofs
5 months ago haftmann 2019-06-14 moved comment to approproiate place
5 months ago haftmann 2019-06-14 removed outcommented example which seems not to work as advertized
5 months ago haftmann 2019-06-14 clear separation of types for bits (False / True) and Z2 (0 / 1)
5 months ago haftmann 2019-06-14 generalized type classes for parity to cover word types also, which contain zero divisors
5 months ago haftmann 2019-06-14 slightly more specialized name for type class
5 months ago haftmann 2019-06-14 dropped weaker legacy alias
5 months ago haftmann 2019-06-14 slightly more stringent ordering of theorems
5 months ago haftmann 2019-06-14 removed relics of ASCII syntax for indexed big operators
5 months ago haftmann 2019-06-14 dropped former legacy input abbreviations
5 months ago haftmann 2019-06-14 using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
5 months ago haftmann 2019-06-14 prefer fixed simpset for proof procedure
5 months ago haftmann 2019-06-14 tuned file system structure
5 months ago haftmann 2019-06-14 avoid spammed sledgehammer proofs
5 months ago nipkow 2019-06-11 added lemmas
5 months ago wenzelm 2019-06-09 proper URL;
5 months ago wenzelm 2019-06-09 merged;
5 months ago wenzelm 2019-06-09 Added tag Isabelle2019 for changeset 83774d669b51
5 months ago blanchet 2019-06-07 handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
5 months ago wenzelm 2019-06-04 tuned;
5 months ago wenzelm 2019-06-04 tuned;