tuned

tuned;

tuned;

tuned;

boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes

merged

start moving actual Jenkins build scripts into the repository

tuned order for isar-ref;

clarified;

clarified syntax;

spelling;

bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;

added command 'unbundle';

Merge

code to catch exception TERM in blast

merged

avoid duplicate Attrib.local_notes in aux. context;

proper restore;

tuned;

tuned;

tuned;

prefer hybrid 'bundle' command;

documentation;

clarified;

support for bundle definition via target;

tuned signature;

tuned;

tuned signature;

tuned;

Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.

merged

approximation, derivative, and continuity of floor and ceiling

remove smt call in Lebesge_Measure

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