isabelle: Graph

refined conversion to only react on proper set comprehensions; tuned
2012-10-17, by bulwahn
moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
2012-10-17, by bulwahn
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
2012-10-17, by bulwahn
another Future.shutdown after Future.cancel_groups (cf. 0d4106850eb2);
2012-10-17, by wenzelm
more robust cancel_now: avoid shooting yourself in the foot;
2012-10-17, by wenzelm
more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;
2012-10-17, by wenzelm
proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
2012-10-17, by wenzelm
added Output "Detach" button;
2012-10-17, by wenzelm
skipped proofs appear as "bad" without counting as error;
2012-10-17, by wenzelm
more method position information, notably finished_pos after end of previous text;
2012-10-17, by wenzelm
more formal markup;
2012-10-17, by wenzelm
tuned signature;
2012-10-17, by wenzelm
more formal markup;
2012-10-17, by wenzelm
don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule
2012-10-17, by kuncar
merged
2012-10-16, by wenzelm
added missing file
2012-10-16, by blanchet
tuned for document output
2012-10-16, by traytel
added proof minimization code from Steffen Smolka
2012-10-16, by blanchet
tuned blank lines
2012-10-16, by traytel
tuned whitespace
2012-10-16, by traytel
a few notations changed in HOL/BNF/Examples/Derivation_Trees
2012-10-16, by popescua
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
2012-10-16, by popescua
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
2012-10-16, by bulwahn
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
2012-10-16, by bulwahn
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
2012-10-16, by bulwahn
extending preprocessing of simproc to rewrite subset inequality into membership of powerset
2012-10-16, by bulwahn
update ROOT with teh directory change in BNF
2012-10-16, by popescua
changed name of BNF/Example directory from Infinite_Derivation_Trees to Derivation_Trees
2012-10-16, by popescua
retain info dockable state via educated guess on window focus;
2012-10-16, by wenzelm
support for more informative errors in lazy enumerations;
2012-10-16, by wenzelm
more informative errors for 'also' and 'finally';
2012-10-16, by wenzelm
tuned messages;
2012-10-16, by wenzelm
more proof method text position information;
2012-10-16, by wenzelm
clarified defer/prefer: more specific errors;
2012-10-16, by wenzelm
updated Toplevel.proofs;
2012-10-16, by wenzelm
more informative errors for 'proof' and 'apply' steps;
2012-10-16, by wenzelm
more friendly handling of Pure.thy bootstrap errors;
2012-10-16, by wenzelm
more informative error for stand-alone 'qed';
2012-10-16, by wenzelm
further attempts to unify/simplify goal output;
2012-10-16, by wenzelm
more informative error messages of initial/terminal proof methods;
2012-10-16, by wenzelm
merged
2012-10-15, by wenzelm
setcomprehension_pointfree simproc also works for set comprehension without an equation
2012-10-15, by bulwahn
tuned message -- avoid extra blank lines;
2012-10-15, by wenzelm
updated to polyml-5.5.0 which reduces chance of HOL-IMP failure (although it is hard to reproduce anyway);
2012-10-15, by wenzelm
store colors after build
2012-10-14, by Markus Kaiser
adding further test cases for the set_comprehension_pointfree simproc
2012-10-14, by bulwahn
refined tactic in set_comprehension_pointfree simproc
2012-10-14, by bulwahn
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
2012-10-14, by bulwahn
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
2012-10-14, by bulwahn
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
2012-10-14, by bulwahn
more informative error of initial/terminal proof steps;
2012-10-13, by wenzelm
some attempts to unify/simplify pretty_goal;
2012-10-13, by wenzelm
refined Proof.the_finished_goal with more informative error;
2012-10-13, by wenzelm
tuned signature;
2012-10-13, by wenzelm
improved adhoc height for small fonts;
2012-10-13, by wenzelm
further refinement of jEdit line range, avoiding lack of final \n;
2012-10-12, by wenzelm
more uniform tooltip color;
2012-10-12, by wenzelm
more NEWS;
2012-10-12, by wenzelm
merged
2012-10-12, by wenzelm
disambiguated grammar
2012-10-12, by traytel
tuned proofs
2012-10-12, by traytel
tuned
2012-10-12, by nipkow
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
2012-10-12, by wenzelm
discontinued typedef with alternative name;
2012-10-12, by wenzelm
discontinued obsolete typedef (open) syntax;
2012-10-12, by wenzelm
discontinued typedef with implicit set_def;
2012-10-12, by wenzelm
merged
2012-10-12, by wenzelm
increading indexes to avoid clashes in the set_comprehension_pointfree simproc
2012-10-12, by bulwahn
no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
2012-10-12, by wenzelm
do not treat interrupt as error here, to avoid confusion in log etc.;
2012-10-12, by wenzelm
more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
2012-10-12, by wenzelm
refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
2012-10-11, by wenzelm
merged
2012-10-11, by wenzelm
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