isabelle: Graph

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
conected CS to big-step
2012-09-21, by nipkow
generate "expand" property
2012-09-21, by blanchet
merge
2012-09-20, by blanchet
finished "disc_coiter_iff" etc. generation
2012-09-20, by blanchet
the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)
2012-09-20, by blanchet
generate coiter_iff and corec_iff theorems
2012-09-20, by blanchet
NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
2012-09-20, by Andreas Lochbihler
more efficient code setup
2012-09-20, by Andreas Lochbihler
added "simp"s to coiter/corec theorems + export under "simps" name
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
tuned
2012-09-20, by nipkow
less rendering (cf. 28bd0709443a) -- avoid conflict with static token markup of different keyword kinds;
2012-09-21, by wenzelm
tuned painter;
2012-09-20, by wenzelm
clarified message background;
2012-09-20, by wenzelm
tuned rendering;
2012-09-20, by wenzelm
no caret painting;
2012-09-20, by wenzelm
text_rendering as managed task, with cancellation;
2012-09-20, by wenzelm
more management of Invoke_Scala tasks;
2012-09-20, by wenzelm
more direct Markup_Tree.from_XML;
2012-09-20, by wenzelm
tuned signature;
2012-09-20, by wenzelm
more direct Markup_Tree.from_XML;
2012-09-20, by wenzelm
tuned signature;
2012-09-20, by wenzelm
tuned;
2012-09-20, by wenzelm
removed lpfp and proved least pfp thm
2012-09-20, by nipkow
provide predicator, define relator
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
adapting "More_BNFs" to new relators/predicators
2012-09-20, by blanchet
fixed infinite loop with trivial rel_O_Gr + tuning
2012-09-20, by blanchet
adapted FP code to new relator approach
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
renamed "bnf_fp_util.ML" to "bnf_fp.ML"
2012-09-20, by blanchet
adapted BNF composition to new relator approach
2012-09-20, by blanchet
don't define relators unless necessary
2012-09-20, by blanchet
moved predicator definition before after_qed
2012-09-20, by blanchet
add rel as first-class citizen of BNF
2012-09-20, by blanchet
renamed "rel_def" to "rel_O_Gr"
2012-09-20, by blanchet
renamed "sum_setl" to "setl" and similarly for r
2012-09-20, by blanchet
tuned ID/DEADID setup
2012-09-20, by blanchet
JavaFX is inactive by default;
2012-09-19, by wenzelm
reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
2012-09-19, by wenzelm
universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);
2012-09-19, by wenzelm
more direct GUI component;
2012-09-19, by wenzelm
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
2012-09-19, by wenzelm
made SML/NJ happy;
2012-09-19, by wenzelm
tuned;
2012-09-19, by wenzelm
merged
2012-09-19, by wenzelm
recording elapsed time in mutabelle for more detailed evaluation
2012-09-19, by bulwahn
Added missing predicators (for multisets and countable sets)
2012-09-18, by popescua
added top-level theory for Cardinals
2012-09-18, by popescua
group "simps" together
2012-09-18, by blanchet
register induct attributes
2012-09-18, by blanchet
further tuned simpset
2012-09-18, by blanchet
bnf_note_all mode for "pre_"-BNFs
2012-09-18, by traytel
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
2012-09-18, by traytel
tuned
2012-09-18, by nipkow
beautified names
2012-09-18, by nipkow
proved all upper bounds
2012-09-18, by nipkow
tuned simpset
2012-09-17, by blanchet
cleaner way of dealing with the set functions of sums and products
2012-09-17, by blanchet
handle the general case with more than two levels of nesting when discharging induction prem prems
2012-09-17, by blanchet
clean unfolding of prod and sum sets
2012-09-17, by blanchet
got rid of one "auto" in induction tactic
2012-09-17, by blanchet
cleaned up internal naming scheme for bnfs
2012-09-17, by traytel
more robust GUI component handlers;
2012-09-19, by wenzelm
more rendering;
2012-09-18, by wenzelm
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
2012-09-18, by wenzelm
output is read-only;
2012-09-18, by wenzelm
token marker for extended syntax styles;
2012-09-18, by wenzelm
pass base_snapshot to enable hyperlinks into other nodes;
2012-09-18, by wenzelm
more explicit message markup and rendering;
2012-09-18, by wenzelm
recover order of stacked markup;
2012-09-18, by wenzelm
some actual rich text markup via XML.content_markup;
2012-09-18, by wenzelm
proper separation of output messages;
2012-09-18, by wenzelm
some support for inital command markup;
2012-09-18, by wenzelm
more static rendering state;
2012-09-18, by wenzelm
Pretty_Text_Area is based on Rich_Text_Area;
2012-09-18, by wenzelm
renamed Text_Area_Painter to Rich_Text_Area;
2012-09-17, by wenzelm
tuned signature -- more general Text_Area_Painter operations;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
somewhat more general JEdit_Lib;
2012-09-17, by wenzelm
prefer official polyml-5.5.0;
2012-09-17, by wenzelm
bypass HOL-Mirabelle-ex in regular test, until its tendency to "hang" has been resolved;
2012-09-17, by wenzelm
merged
2012-09-17, by wenzelm
tuned
2012-09-17, by nipkow
updated to polyml-5.5.0;
2012-09-17, by wenzelm
some updates for polyml-5.5.0;
2012-09-17, by wenzelm
tuned
2012-09-17, by nipkow
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
2012-09-16, by wenzelm
got rid of ad-hoc lift function
2012-09-16, by nipkow
converted wt into a set, tuned names
2012-09-16, by nipkow
use strip_typeN in bnf_def (instead of repairing strip_type)
2012-09-16, by traytel
removing find_theorems commands that were left in the developments accidently
2012-09-16, by bulwahn
tuning
2012-09-15, by blanchet
tuned code to avoid special case for "fun"
2012-09-15, by blanchet
tuned induction tactic
2012-09-15, by blanchet
tuned error message
2012-09-15, by blanchet
tuning
2012-09-15, by blanchet
typeclass formalising bounded subtraction
2012-09-15, by haftmann
dropped some unused identifiers
2012-09-15, by haftmann
export rel_mono theorem
2012-09-15, by traytel
merged two unfold steps
2012-09-14, by blanchet
took out one rotate_tac
2012-09-14, by blanchet
killed spurious rotate_tac; use auto instead of blast
2012-09-14, by blanchet
moved blast tactic to where it is actually needed
2012-09-14, by blanchet
fixed bug in "mk_map" for the "fun" case
2012-09-14, by blanchet
correct generalization to 3 or more mutually recursive datatypes
2012-09-14, by blanchet
provide more guidance, exploiting our knowledge of the goal
2012-09-14, by blanchet
fixed issue with bound variables in prem prems + tuning
2012-09-14, by blanchet
use right version of "mk_UnIN"
2012-09-14, by blanchet
select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
2012-09-14, by blanchet
tuned code before fixing "mk_induct_discharge_prem_prems_tac"
2012-09-14, by blanchet
tuned proofs;
2012-09-14, by wenzelm
merged
2012-09-14, by wenzelm
polished the induction
2012-09-14, by blanchet
put the flat at the right place (to avoid exceptions)
2012-09-14, by blanchet
fixed variable exporting problem
2012-09-14, by blanchet
compile
2012-09-14, by blanchet
added induct tactic
2012-09-14, by blanchet
tuning
2012-09-14, by blanchet
renamed "mk_UnN" to "mk_UnIN"
2012-09-14, by blanchet
merged two commands
2012-09-14, by blanchet
allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
2012-09-14, by blanchet
distinguish between nested and nesting BNFs
2012-09-14, by blanchet
make tactic more robust in the case where "asm_simp_tac" already finishes the job
2012-09-14, by blanchet
derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive
2012-09-14, by blanchet
no longer react on global_settings (cf. 34ac36642a31);
2012-09-14, by wenzelm
refined output panel: more value-oriented approach to update and caret focus;
2012-09-14, by wenzelm
clarified markup names;
2012-09-14, by wenzelm
more general Document_Model.point_range;
2012-09-14, by wenzelm
more static handling of rendering options;
2012-09-14, by wenzelm
tuned options (again);
2012-09-14, by wenzelm
more scalable option-group;
2012-09-14, by wenzelm
tuned
2012-09-14, by nipkow
merged
2012-09-13, by wenzelm
tuned proofs;
2012-09-13, by wenzelm
remove theory Real_Integration, not needed since 44e42d392c6e when Euclidean spaces where introduced
2012-09-13, by hoelzl