isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle