isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

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
renamed ML file in preparation for next step
2012-09-28, by blanchet
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
2012-09-28, by blanchet
modernized example, exploiting "rep_compat" option
2012-09-28, by blanchet
compatibility option to use "rep_datatype"
2012-09-28, by blanchet
tuned message
2012-09-28, by blanchet
modernized example
2012-09-28, by blanchet
tuned tactics
2012-09-28, by traytel
second usage of const_typ
2012-09-28, by nipkow
new antiquotation const_typ
2012-09-28, by nipkow
tuned printing of _ in latex
2012-09-28, by nipkow
mk_readable_rsp_thm_eq is more robust now
2012-09-27, by kuncar
new get function for non-symmetric relator_eq & tuned
2012-09-27, by kuncar
merged
2012-09-27, by wenzelm
tuned tactic; got rid of substs_tac alias
2012-09-27, by traytel
use a nicer scheme to indexify names
2012-09-27, by blanchet
tuned tactic
2012-09-27, by traytel