isabelle: Graph

cleanup borel_measurable_positive_integral_(fst|snd)
2012-10-11, by hoelzl
msetprod based directly on Multiset.fold;
2012-10-11, by haftmann
avoid global interpretation
2012-10-11, by haftmann
simplified construction of fold combinator on multisets;
2012-10-11, by haftmann
clarified output token markup (see also bc22daeed49e);
2012-10-11, by wenzelm
refined aprop_tr' -- retain entity information by using type slot as adhoc marker;
2012-10-11, by wenzelm
refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
more position information for hyperlink and placement of message;
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
2012-10-11, by krauss
removed unused legacy material from mira.py
2012-10-10, by krauss
eliminated some remaining uses of typedef with implicit set definition;
2012-10-10, by wenzelm
merged
2012-10-10, by Andreas Lochbihler
fix code equation for RBT_Impl.fold
2012-10-10, by Andreas Lochbihler
merged
2012-10-10, by Andreas Lochbihler
tail-recursive implementation for length
2012-10-10, by Andreas Lochbihler
correct definition for skip_black
2012-10-10, by Andreas Lochbihler
merged
2012-10-10, by wenzelm
merged
2012-10-10, by hoelzl
infprod generator works also with empty index set
2012-10-10, by hoelzl
add finite entropy
2012-10-10, by hoelzl
continuous version of mutual_information_eq_entropy_conditional_entropy
2012-10-10, by hoelzl
add induction for real Borel measurable functions
2012-10-10, by hoelzl
induction prove for positive_integral_fst
2012-10-10, by hoelzl
strong nonnegativ (instead of ae nn) for induction rule
2012-10-10, by hoelzl
induction prove for positive_integral_density
2012-10-10, by hoelzl
add induction rules for simple functions and for Borel measurable functions
2012-10-10, by hoelzl
introduce induction rules for simple functions and for Borel measurable functions
2012-10-10, by hoelzl
joint distribution of independent variables
2012-10-10, by hoelzl
indep_vars does not need sigma-sets
2012-10-10, by hoelzl
simplified definitions
2012-10-10, by hoelzl
remove unnecessary assumption from conditional_entropy_eq
2012-10-10, by hoelzl
alternative definition of conditional entropy
2012-10-10, by hoelzl
remove unneeded assumption from conditional_entropy_generic_eq
2012-10-10, by hoelzl
add induction rule for intersection-stable sigma-sets
2012-10-10, by hoelzl
show and use distributed_swap and distributed_jointI
2012-10-10, by hoelzl
rule to show that conditional mutual information is non-negative in the continuous case
2012-10-10, by hoelzl
continuous version of entropy_le
2012-10-10, by hoelzl
simplified entropy_uniform
2012-10-10, by hoelzl
remove incseq assumption from measure_eqI_generator_eq
2012-10-10, by hoelzl
generalize from prob_space to finite_measure
2012-10-10, by hoelzl
add measurable_compose
2012-10-10, by hoelzl
simplified assumptions for kolmogorov_0_1_law
2012-10-10, by hoelzl
merge should operate on pairs
2012-10-10, by hoelzl
remove incseq assumption from sigma_prod_algebra_sigma_eq
2012-10-10, by hoelzl
sigma_finite_iff_density_finite does not require a positive density function
2012-10-10, by hoelzl
tuned Lebesgue measure proofs
2012-10-10, by hoelzl
tuned product measurability
2012-10-10, by hoelzl
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
2012-10-10, by hoelzl
use continuity to show Borel-measurability
2012-10-10, by hoelzl
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
2012-10-10, by hoelzl
rename terminal_events to tail_event
2012-10-10, by hoelzl
merged
2012-10-10, by Andreas Lochbihler
efficient construction of red black trees from sorted associative lists
2012-10-10, by Andreas Lochbihler
more explicit code equations
2012-10-10, by haftmann
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
2012-10-10, by bulwahn
special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)
2012-10-10, by bulwahn
test case for set_comprehension_pointfree simproc succeeds now
2012-10-10, by bulwahn
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
2012-10-10, by bulwahn
moving simproc from Finite_Set to more appropriate Product_Type theory
2012-10-10, by bulwahn
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
2012-10-10, by bulwahn
adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc
2012-10-10, by bulwahn
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
2012-10-10, by bulwahn
more consistent error messages on malformed code equations
2012-10-10, by haftmann
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
2012-10-09, by huffman
use Set.filter instead of Finite_Set.filter, which is removed then
2012-10-09, by kuncar
rename Set.project to Set.filter - more appropriate name
2012-10-09, by kuncar
added some ad-hoc namespace prefixes to avoid duplicate facts;
2012-10-10, by wenzelm
avoid duplicate facts;
2012-10-10, by wenzelm
more explicit namespace prefix for 'statespace' -- duplicate facts;
2012-10-10, by wenzelm
eliminated spurious fact duplicates;
2012-10-10, by wenzelm
modernized dynamic "rules" -- avoid rebinding of static facts;
2012-10-10, by wenzelm
removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
2012-10-09, by wenzelm
clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
2012-10-09, by wenzelm
tuned;
2012-10-09, by wenzelm
clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
2012-10-09, by wenzelm
more explicit flags for facts table;
2012-10-09, by wenzelm
minor tuning;
2012-10-09, by wenzelm
more conventional Double constants;
2012-10-09, by wenzelm
tuned source structure;
2012-10-09, by wenzelm
tuned;
2012-10-09, by wenzelm
tuned;
2012-10-09, by wenzelm
merged
2012-10-09, by wenzelm
added type annotations to generated Isar proofs -- code by Steffen Smolka
2012-10-09, by blanchet
consolidated names of theorems on composition;
2012-10-08, by haftmann
corrected NEWS
2012-10-08, by haftmann
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
2012-10-08, by wenzelm
clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
2012-10-08, by wenzelm
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
2012-10-08, by wenzelm
tuned;
2012-10-08, by wenzelm
prefer synchronous Mutator_Event.Bus on Swing_Thread;
2012-10-08, by wenzelm
more direct tooltip content;
2012-10-08, by wenzelm
tuned;
2012-10-08, by wenzelm
use Pretty_Tooltip for Graphview_Panel;
2012-10-08, by wenzelm
more basic tooltips;
2012-10-08, by wenzelm
close tooltips more thoroughly;
2012-10-07, by wenzelm
make buttons closer to original mouse position;
2012-10-07, by wenzelm
detach tooltip as dockable window;
2012-10-07, by wenzelm
explicit close button;
2012-10-07, by wenzelm
congruence rule for Finite_Set.fold
2012-10-06, by haftmann
alternative simplification of ^^ to the righthand side;
2012-10-06, by haftmann
eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;
2012-10-05, by wenzelm
merged
2012-10-05, by wenzelm
newer versions of Z3 call it "Bool" not "bool"
2012-10-05, by blanchet
simplified type of msetprod;
2012-10-04, by haftmann
tuned proof
2012-10-04, by haftmann
default simp rule for image under identity
2012-10-04, by haftmann
dropped duplicate facts; tuned syntax
2012-10-04, by haftmann
more facts on setsum and setprod
2012-10-04, by haftmann
made SML/NJ happier
2012-10-04, by traytel
do not expose details of internal data structures for composition of BNFs
2012-10-04, by traytel
further support for nested tooltips;
2012-10-05, by wenzelm
tuned proofs;
2012-10-05, by wenzelm
refer to parent frame -- relevant for floating dockables in particular;
2012-10-05, by wenzelm
tuned window position to fit on screen;
2012-10-05, by wenzelm
tuned window position;
2012-10-05, by wenzelm
determine window size from content;
2012-10-05, by wenzelm
tuned color and font size;
2012-10-05, by wenzelm