proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);

merged

NEWS;

tuned proofs;

provide dynamic facts in static context, to allow use of method_facts during static closure;

tuned;

clarified signature;

less ambitious arguments: thms only, no context declaration;

added method operator "use";

clarified signature;

clean facts more uniformly;

expode method_facts via dynamic method context;

tuned;

generalized bitlen to floor of log

repair Unicode mess-up in c493859d4267

NEWS and CONTRIBUTORS for SPMF

merged

import wasysym needed by Rewrite.thy

add theory of discrete subprobability distributions

clear distinction between different situations concerning strictness of code equations

tuned signature

more correct exception handling

explicit tagging of code equations de-baroquifies interface

dropped unused code

conventional syntax for unit abstractions

added action "isabelle.select-entity";

tuned;

clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;

tuned;

less redundant exploration of full name space;

tuned;

avoid multiple reports on shared type;

updated to recent changes of Poly/ML directory layout;

tuned;

Integer.lcm normalizes the sign as in HOL/GCD.thy; tuned;

support for .scala tools;

move ennreal and ereal theorems from MFMC_Countable

more flexible build_selection;

clarified aliases (no warning for duplicates);

eliminated pointless alias (no warning for duplicates);

avoid warnings on duplicate rules in the given list;

avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;

Hid RBT.filter

proper ceil operation;

tuned;

isabelle components_checksum -u;

more documentation;

updated to jdk-8u92;

merged

NEWS;

more adhoc overloading; eliminated pointless Rat.eq: this is an equality type; tuned;

clarified exception -- actually reject denominator = 0;

ML pp for Rat.rat;

clarified string_of_rat operations;

tuned signature;

clarified signature;

prefer rat numberals;

support rat numerals via special antiquotation syntax;

tuned signature;

tuned;

tuned signature;

maintain invariant for exported operation;

prefer more efficient Poly/ML operations, taking care of sign;

ad-hoc overloading for standard operations on type Rat.rat;

rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;

Merged

Tuned code equations for mappings and PMFs

Added code generation for PMFs

merged

moved lemma from afp

ignore Maven build products

added test

made parsing of monomorphic/polymorphic constants more robust

more flexible parsing (towards type class support)

error message

allow multiple recursive methods to co-exist in order to support mutual recursion;

apply current morphism to method text before evaluating;

merged

tuned;

allow 'for' fixes for multi_specs;

unused;

clarified check_open_spec / read_open_spec; allow 'for' fixes in 'abbreviation', 'definition';

tuned;

clarified 'axiomatization';

clarified axiomatization;

clarified axiomatization: proper variables (!);

explicit check that abstract constructors cannot be part of official interface

do not export abstract constructors in code_reflect

added subtheory of longest common prefix

tuned proofs;

tuned proofs;

tuned proofs, to allow unfold_abs_def;

clarified "unfold" operations;

tuned proof;

isabelle update_cartouches -c -t;

tuned spelling;

examples and documentation for code generator time measurements

optional timing for code generator conversions

clarified internal interfaces

tuned

delegate inclusion of required dictionaries to user-space instead of half-working magic

corrected closure scope of static_conv_thingol; clarified implementation and names

clarified proof context vs. background theory

explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv

clarified naming conventions and code for code evaluation sandwiches

clarified names of variants

added function "prefixes" and some lemmas

Merge

Merge

moved two theorems

updated proof of Residue Theorem (form Wenda Li)

merged

renamed suffix(eq)

updated 'define';

merged

isabelle update_cartouches -c -t;

isabelle update_cartouches -c -t;

NEWS: Permutations of a set and randomised folds

new Isabelle component for CI infastructure

merged

recovered printing of DIM('a) (cf. 899c9c4e4a4c);

updated;

simplified syntax;

clarified syntax category names according to Isabelle/ML/Scala;

simplified syntax: Parse.term corresponds to Args.term etc.;

clarified syntax categories;

cartouche abbreviations work both for " as well;

Removed problematic code equation for set_permutations

Backed out changeset 8230358fab88

Deleted problematic code equation in Codegenerator_Test

Merge

New theory for Homeomorphisms

Merge

renamings and new material

new theorem

deleted stray thm command

deleted needless comment

Resolved cyclic dependency of theories

Merged

Added set permutations/random permutations

merged

embedded content may be delimited via cartouches;

tuned;

merged

renamed prefix* in Library/Sublist

generate Vampire 4.0 compatible output

Merge

Lots of new material for multivariate analysis

removed odd cases rule (see also 8cb42cd97579);

tuned proofs;

tuned document;

misc tuning and modernization;

proper document source; tuned proofs;

misc tuning and modernization;

merged

added timing lemmas

uniformly continuous function extended continuously on closure

reduce isUCont to uniformly_continuous_on

removed smt proof

better handling of veriT's 'unknown' status

Resolved name clash

Merged

Moved material from AFP/Randomised_Social_Choice to distribution

Library: add partition_on

proper consideration of chained facts in 'try0' minimization

re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);

tuned;

toplevel theorem statements support 'if'/'for' eigen-context;

reverted accidental commit;

eliminated use of empty "assms";

more complete theories;

common entity definitions within a global or local theory context;

clarified heading

a quasi-recursive characterization of the multiset order (by Christian Sternagel)

merged

avoid spurious fact index, notably in "context begin" (via Bundle.context);

tuned;

tuned;

tuned;

expose Sessions.Info in Build.Results

introduced class topological_group between topological_monoid and real_normed_vector

find dynamic facts as well, but static ones are preferred; tuned;

some slight generalizations

Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman Minkowski theorem

two new lemmas about segments

Merge

lemmas about dimension, hyperplanes, span, etc.

merged

clarified context, notably for internal use of Simplifier;

renamings and refinements

move Stirling numbers from AFP/Discrete_Summation

the standard While-rule