isabelle: Graph

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
tuned color and font size;
2012-10-05, by wenzelm
close tooltip window on escape;
2012-10-05, by wenzelm
proper message markup for output;
2012-10-05, by wenzelm
some re-ordering of initialization to ensure proper formatting;
2012-10-04, by wenzelm
separate module Pretty_Tooltip;
2012-10-04, by wenzelm
refined rich tooltip options;
2012-10-04, by wenzelm
Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;
2012-10-04, by wenzelm
some documentation of show_markup;
2012-10-04, by wenzelm
tuned proofs;
2012-10-04, by wenzelm
option to bypass potentially slow text overview;
2012-10-04, by wenzelm
tuned signature;
2012-10-04, by wenzelm
clarified platform dependency;
2012-10-04, by wenzelm
updated crontab and afp-poly settings
2012-10-04, by Gerwin Klein
thread the right local theory through + reenable parallel proofs for previously problematic theories
2012-10-03, by blanchet
made code more conform to rest of BNF package
2012-10-03, by blanchet
more error positions;
2012-10-03, by wenzelm
more explicit show_type_constraint, show_sort_constraint;
2012-10-03, by wenzelm
recovered print translation after 'a => bool to 'a set change;
2012-10-03, by wenzelm
tuned;
2012-10-03, by wenzelm
use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
2012-10-03, by wenzelm
printed "_ofsort" is subject to show_markup as well;
2012-10-03, by wenzelm
allow position constraints to coexist with 0 or 1 sort constraints;
2012-10-03, by wenzelm
made tactic more robust (less usage of stac)
2012-10-02, by traytel
continued changing type of corec type
2012-10-02, by blanchet
removed dead params and dead code
2012-10-02, by blanchet
changed type of corecursor for the nested recursion case
2012-10-02, by blanchet
made (co)rec tactic more robust when the simplifier succeeds early
2012-10-02, by blanchet
tuned;
2012-10-01, by wenzelm
removed unused module Blob;
2012-10-01, by wenzelm
more direct message header: eliminated historic encoding via single letter;
2012-10-01, by wenzelm
tuned whitespace;
2012-10-01, by wenzelm
tuned proofs;
2012-10-01, by wenzelm
report sort assignment of visible type variables;
2012-10-01, by wenzelm
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
2012-10-01, by wenzelm
fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
2012-10-01, by blanchet
tweaked corecursor/coiterator tactic
2012-10-01, by blanchet
changed the type of the recursor for nested recursion
2012-10-01, by blanchet
fixed quick-and-dirty mode
2012-09-30, by blanchet
tuning
2012-09-30, by blanchet
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
2012-09-30, by traytel
got rid of subst_tac alias
2012-09-30, by traytel
tuned tactic
2012-09-30, by traytel
tuned proofs;
2012-09-29, by wenzelm
tuned proofs;
2012-09-29, by wenzelm
proper handling of constraints stemming from idtyp_ast_tr';
2012-09-29, by wenzelm
enable show_markup by default (approx. double output size);
2012-09-29, by wenzelm
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-09-29, by wenzelm
explicit show_types takes preferenced over show_markup;
2012-09-29, by wenzelm
ignore wrapped markup elements in Proof General;
2012-09-29, by wenzelm
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
2012-09-29, by wenzelm
treat wrapped markup elements as raw markup delimiters;
2012-09-29, by wenzelm
tuned signature;
2012-09-29, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned;
2012-09-28, by wenzelm
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-28, by wenzelm
merged
2012-09-28, by wenzelm
eliminated dead code;
2012-09-28, by wenzelm
smarter handling of tracing messages;
2012-09-28, by wenzelm
display number of tracing messages;
2012-09-28, by wenzelm
tuned signature;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
simplified simpset
2012-09-28, by blanchet
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
2012-09-28, by blanchet
tuned tactic
2012-09-28, by traytel
updated keywords using proper "isabelle update_keywords";
2012-09-28, by wenzelm
tuned tactic
2012-09-28, by traytel
tuned tactic
2012-09-28, by traytel
merge
2012-09-28, by blanchet