isabelle: Graph

tuned
2012-09-27, by nipkow
operations to turn markup into XML;
2012-09-27, by wenzelm
removed obsolete org.w3c.dom operations;
2012-09-27, by wenzelm
eliminated obsolete HTML/CSS functionality;
2012-09-27, by wenzelm
removed obsolete Output1 dockable;
2012-09-27, by wenzelm
physical File.eq in conformance to Isabelle/ML;
2012-09-27, by wenzelm
tuned proofs;
2012-09-27, by wenzelm
tuned;
2012-09-27, by wenzelm
updated to consolidated SortedMap in scala-2.9.x;
2012-09-27, by wenzelm
partly ported "TreeFI" example to new syntax
2012-09-27, by blanchet
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
2012-09-27, by blanchet
tuned
2012-09-27, by nipkow
tuned
2012-09-27, by nipkow
merge
2012-09-27, by blanchet
modernized examples;
2012-09-27, by blanchet
some support for jEdit warmstart;
2012-09-26, by wenzelm
discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
2012-09-26, by wenzelm
tuned message;
2012-09-26, by wenzelm
merged
2012-09-26, by wenzelm
disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)
2012-09-26, by blanchet
got rid of other instance of shaky "Thm.generalize"
2012-09-26, by blanchet
tweaked theorem names (in particular, dropped s's)
2012-09-26, by blanchet
get rid of shaky "Thm.generalize"
2012-09-26, by blanchet
fixed "rels" + split them into injectivity and distinctness
2012-09-26, by blanchet
generate high-level "coinduct" and "strong_coinduct" properties
2012-09-26, by blanchet
added coinduction tactic
2012-09-26, by blanchet
generalized tactic a bit
2012-09-26, by blanchet
export "dtor_map_coinduct" theorems, since they're used in one example
2012-09-26, by blanchet
name tuning
2012-09-26, by blanchet
parameterized "subst_tac"
2012-09-26, by blanchet
generate high-level "maps", "sets", and "rels" properties
2012-09-26, by blanchet
use singular since there is always only one theorem
2012-09-26, by blanchet
nicer type var names
2012-09-26, by blanchet
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
2012-09-26, by blanchet
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
2012-09-26, by blanchet
leave out some internal theorems unless "bnf_note_all" is set
2012-09-26, by blanchet
tuned
2012-09-26, by nipkow
added counterexamples
2012-09-26, by nipkow
tuned
2012-09-26, by nipkow
tuned
2012-09-25, by nipkow
more uniform graphview terminology;
2012-09-26, by wenzelm
proper Symbol.decode -- especially relevant for Proof General;
2012-09-26, by wenzelm
suppress empty tooltips;
2012-09-26, by wenzelm
obsolete;
2012-09-26, by wenzelm
updated keywords;
2012-09-26, by wenzelm
more uniform graphview terminology;
2012-09-26, by wenzelm
tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
2012-09-26, by wenzelm
proper install_fonts;
2012-09-26, by wenzelm
proper jvmpath for Windows;
2012-09-25, by wenzelm
basic integration of graphview into document model;
2012-09-25, by wenzelm
ML support for generic graph display, with browser and graphview backends (via print modes);
2012-09-25, by wenzelm
tuned;
2012-09-25, by wenzelm
more complete build;
2012-09-25, by wenzelm
proper error message;
2012-09-25, by wenzelm
separate module Graph_Display;
2012-09-25, by wenzelm
added graph encode/decode operations;
2012-09-25, by wenzelm
tuned;
2012-09-25, by wenzelm
minimal component and build setup for graphview;
2012-09-24, by wenzelm
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
2012-09-24, by Markus Kaiser
made smlnj even happier
2012-09-24, by haftmann
tuned proofs;
2012-09-24, by wenzelm
more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
2012-09-24, by wenzelm
updated checksum, which appears to have changed accidentally;
2012-09-24, by wenzelm
updated to exec_process-1.0.2;
2012-09-24, by wenzelm
search bash via PATH as usual (this is no longer restricted to Cygwin with its known file-system layout);
2012-09-24, by wenzelm
discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);
2012-09-24, by wenzelm
Mirabelle appears to work better in single-threaded mode;
2012-09-24, by wenzelm
generalized types
2012-09-24, by nipkow
tuned termination proof
2012-09-24, by nipkow
adapted examples to new names
2012-09-23, by blanchet
renamed coinduction principles to have "dtor" in the name
2012-09-23, by blanchet
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed "map_simps" to "{c,d}tor_maps"
2012-09-23, by blanchet
took out accidentally submitted "tracing" calls
2012-09-23, by blanchet
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)
2012-09-23, by blanchet
simplified fact policies
2012-09-23, by blanchet
generate "rel_as_srel" and "rel_flip" properties
2012-09-23, by blanchet
started work on generation of "rel" theorems
2012-09-23, by blanchet
make smlnj happy
2012-09-23, by haftmann
more strict typscheme_equiv check: must fix variables of more specific type;
2012-09-22, by haftmann
cache should not contain material from descendant theory
2012-09-22, by haftmann
some PIDE NEWS from this summer;
2012-09-22, by wenzelm
tuned whitespace;
2012-09-22, by wenzelm
tuned;
2012-09-22, by wenzelm
tuned proofs;
2012-09-22, by wenzelm
report proper binding positions only -- avoid swamping document model with unspecific information;
2012-09-22, by wenzelm
accumulate under exec_id as well;
2012-09-22, by wenzelm
more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
2012-09-22, by wenzelm
misc tuning;
2012-09-22, by wenzelm
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
2012-09-22, by wenzelm
tuned signature;
2012-09-22, by wenzelm
tuned proofs;
2012-09-21, by wenzelm
misc tuning;
2012-09-21, by wenzelm
tighten margin for TextArea instead of Lobo;
2012-09-21, by wenzelm
misc tuning;
2012-09-21, by wenzelm
renamed LFP low-level rel property to have ctor not dtor in its name
2012-09-21, by blanchet
changed base session for "HOL-BNF" for faster building in the typical case
2012-09-21, by blanchet
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
2012-09-21, by blanchet
fixed a few names that escaped the renaming
2012-09-21, by blanchet
tuned whitespace
2012-09-21, by blanchet
merged
2012-09-21, by wenzelm
clean up lemmas used for composition
2012-09-21, by blanchet
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
2012-09-21, by blanchet
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
2012-09-21, by blanchet
renamed top-level theory from "Codatatype" to "BNF"
2012-09-21, by blanchet
adapted examples to renamings
2012-09-21, by blanchet
renamed "pred" to "rel" (relator)
2012-09-21, by blanchet
renamed "rel" to "srel"
2012-09-21, by blanchet
fixed bug introduced by fold/unfold renaming
2012-09-21, by blanchet
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
2012-09-21, by blanchet
simplified code
2012-09-21, by blanchet
tuned a few ML names
2012-09-21, by blanchet
renamed "fld"/"unf" to "ctor"/"dtor"
2012-09-21, by blanchet
tuning
2012-09-21, by blanchet
renamed "upto" coinduction "strong"
2012-09-21, by blanchet
tuned variable names
2012-09-21, by blanchet
tuned names
2012-09-21, by nipkow
more termination proofs
2012-09-21, by nipkow
rel_Gr does not depend on map_wpull
2012-09-21, by traytel
renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
2012-09-21, by wenzelm
more realistic sendback: pick exec_id from message position and text from buffer;
2012-09-21, by wenzelm
some support for hovering and sendback area;
2012-09-21, by wenzelm
merged
2012-09-21, by wenzelm
tuned antiquotations
2012-09-21, by traytel
merged
2012-09-21, by wenzelm
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
2012-09-21, by traytel