isabelle: Graph

less ambitious isatest: polyml-5.3.0 has problems with big sessions like HOL-Proofs;
2014-11-02, by wenzelm
modernized header uniformly as section;
2014-11-02, by wenzelm
prefer \setisabellecontext;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
obsolete;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
obsolete;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
clarified legacy command;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
obsolete;
2014-11-02, by wenzelm
added update_header tool;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
more flexibile \setisabellecontext, independently of header;
2014-11-02, by wenzelm
prefer explicit heading command;
2014-11-02, by wenzelm
uniform heading commands work in any context, even in theory header;
2014-11-02, by wenzelm
eliminated dead code;
2014-11-02, by wenzelm
clarified syntax -- avoid overlap with command category;
2014-11-01, by wenzelm
tuned signature (see ab2483fad861);
2014-11-01, by wenzelm
recover via scanner;
2014-11-01, by wenzelm
simplified -- scanning is never interactive;
2014-11-01, by wenzelm
tuned signature, in accordance to Scala version;
2014-11-01, by wenzelm
command-line terminator ";" is no longer accepted;
2014-11-01, by wenzelm
eliminated spurious semicolons;
2014-11-01, by wenzelm
eliminated former Proof General preferences;
2014-11-01, by wenzelm
merged
2014-10-31, by wenzelm
tuned;
2014-10-31, by wenzelm
provide explicit theory (amending 621c052789b4);
2014-10-31, by wenzelm
removed pointless markup;
2014-10-31, by wenzelm
discontinued obsolete \<^sync> marker;
2014-10-31, by wenzelm
discontinued obsolete control command category;
2014-10-31, by wenzelm
obsolete;
2014-10-31, by wenzelm
obsolete;
2014-10-31, by wenzelm
discontinued obsolete tty and prompt;
2014-10-31, by wenzelm
discontinued pointless option: timing is always on (overall theory only);
2014-10-31, by wenzelm
eliminated odd flags and hook;
2014-10-31, by wenzelm
avoid noise (cf. 03ff4d1e6784);
2014-10-31, by wenzelm
discontinued Isar TTY loop;
2014-10-31, by wenzelm
removed obsolete Proof General commands;
2014-10-31, by wenzelm
obsolete;
2014-10-31, by wenzelm
discontinued obsolete Output.urgent_message;
2014-10-31, by wenzelm
discontinued Proof General;
2014-10-31, by wenzelm
Some comments and a new version of a result
2014-10-31, by paulson
merged
2014-10-30, by wenzelm
eliminated aliases;
2014-10-30, by wenzelm
eliminated aliases;
2014-10-30, by wenzelm
eliminated aliases;
2014-10-30, by wenzelm
tuned spelling;
2014-10-30, by wenzelm
hardwired imitation of copy.shortcut2 default;
2014-10-30, by wenzelm
more simp rules concerning dvd and even/odd
2014-10-30, by haftmann
choose_reduce_nat: re-ordered operands
2014-10-30, by paulson
make SML/NJ more happy;
2014-10-30, by wenzelm
proper syntax categery "name" -- as usual and as documented;
2014-10-30, by wenzelm
disable coercions for NO_MATCH
2014-10-30, by hoelzl
merged
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
merged
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
tuned;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
more standard theory name;
2014-10-29, by wenzelm
more iterators;
2014-10-29, by wenzelm
removed useless lemmas
2014-10-29, by nipkow
tuned layout and proofs
2014-10-29, by nipkow
tuned proofs;
2014-10-28, by wenzelm
increase chances that HOL-Proofs image still works for polyml-5.3.0;
2014-10-28, by wenzelm
tuned signature;
2014-10-28, by wenzelm
proper selectMatch, e.g. relevant for S-click on gutter;
2014-10-28, by wenzelm
find command span in buffer;
2014-10-28, by wenzelm
'notepad' requires proper nesting of begin/end;
2014-10-28, by wenzelm
explicit keyword category for commands that may start a block;
2014-10-28, by wenzelm
updated keywords;
2014-10-28, by wenzelm
'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
2014-10-28, by wenzelm
more abstract type;
2014-10-28, by wenzelm
tuned;
2014-10-28, by wenzelm
tuned;
2014-10-28, by wenzelm
updated to jdk-7u72;
2014-10-27, by wenzelm
increase chances that HOL-Proofs image still works for polyml-5.3.0;
2014-10-27, by wenzelm
JRE is sufficient for official release -- javac and jar are only needed for self-build;
2014-10-27, by wenzelm
clarified ISABELLE_JDK_HOME vs. JAVA_HOME;
2014-10-27, by wenzelm
ISABELLE_JAVA_EXT is obsolete;
2014-10-27, by wenzelm
further generalization of natfloor_div_nat
2014-10-27, by hoelzl
generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
2014-10-27, by hoelzl
eliminated redundancies;
2014-10-26, by haftmann
more simp rules;
2014-10-25, by haftmann
clarified default;
2014-10-26, by wenzelm
support negative extraLineSpacing;
2014-10-26, by wenzelm
tuned whitespace;
2014-10-25, by wenzelm
made SML/NJ happy;
2014-10-25, by wenzelm
merged;
2014-10-24, by wenzelm
discontinued python from standard system environment;
2014-10-24, by wenzelm
more generous default;
2014-10-24, by wenzelm
even further downshift of theory Parity in the hierarchy
2014-10-23, by haftmann
further downshift of theory Parity in the hierarchy
2014-10-23, by haftmann
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-10-24, by hoelzl
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
2014-10-24, by hoelzl
repaired long-standing accident
2014-10-23, by haftmann
explicit definition restores HOL Light import after cb9d84d3e7f2
2014-10-23, by haftmann
tuned language and spelling
2014-10-23, by haftmann
slight generalization and unification of simp rules for algebraic procedures
2014-10-23, by haftmann
downshift of theory Parity in the hierarchy
2014-10-23, by haftmann
parity induction over natural numbers
2014-10-23, by haftmann
merged
2014-10-22, by wenzelm
proper line height and text base line, like regular TextAreaPainter.PaintText;
2014-10-22, by wenzelm
tuned imports;
2014-10-22, by wenzelm
merged
2014-10-22, by Andreas Lochbihler
add print translation for probability notation \<P>
2014-10-22, by Andreas Lochbihler
find main command keyword of 'begin';
2014-10-22, by wenzelm
restricted scanning;
2014-10-22, by wenzelm
repaired rail diagram (cf. 8450b944e58a);
2014-10-22, by wenzelm
foldPainter like Windows L&F;
2014-10-21, by wenzelm
merged
2014-10-21, by wenzelm
NEWS;
2014-10-21, by wenzelm
tuned whitespace;
2014-10-21, by wenzelm
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
2014-10-21, by wenzelm
support for proof structure matching;
2014-10-21, by wenzelm
tuned;
2014-10-21, by wenzelm
tuned;
2014-10-21, by wenzelm
support for begin/end matching;
2014-10-21, by wenzelm
proper token kind;
2014-10-21, by wenzelm
added option jedit_structure_limit;
2014-10-21, by wenzelm
some structure matching, based on line token iterators;
2014-10-21, by wenzelm
support for structure matching;
2014-10-21, by wenzelm
tuned rendering;
2014-10-21, by wenzelm
back to alternative fold painter, despite f03a9c57760a -- gutter painter seems to have changed in the meantime;
2014-10-21, by wenzelm
tuned;
2014-10-21, by wenzelm
update_cartouches;
2014-10-21, by wenzelm
clarified tree root;
2014-10-21, by wenzelm
tuned spacing;
2014-10-21, by wenzelm
clarified verbatim line breaks, e.g. relevant for Implementation mldecls;
2014-10-21, by wenzelm
turn even into an abbreviation
2014-10-21, by haftmann
update documentation for 'size_o_map'
2014-10-21, by desharna
rename 'size_o_map' to 'size_gen_o_map'
2014-10-21, by desharna
document 'size_gen'
2014-10-21, by desharna
generate 'size_gen' for datatypes
2014-10-21, by desharna
document 'map_o_corec'
2014-10-21, by desharna
generate 'map_o_corec' for (co)datatypes
2014-10-21, by desharna
move documentation of 'rec_o_map'
2014-10-21, by desharna
move theorem 'rec_o_map'
2014-10-21, by desharna
warn for not fully mutually (co)recursive types
2014-10-21, by desharna
add transfer rule for set_pmf
2014-10-21, by hoelzl
add tendsto_const and tendsto_ident_at as simp and intro rules
2014-10-20, by hoelzl
tuned spacing;
2014-10-20, by wenzelm
avoid odd ligatures;
2014-10-20, by wenzelm
more accurate approximation of AST;
2014-10-20, by wenzelm
tuned exposition of {* ... *};
2014-10-20, by wenzelm
more antiquotations;
2014-10-20, by wenzelm
more antiquotations;
2014-10-20, by wenzelm
register transfer rules from BNF and FP_Sugar
2014-10-20, by kuncar
refactored
2014-10-20, by kuncar
merged
2014-10-20, by wenzelm
back to formal comment (see 23a380cc45f4, 3094b0edd6b5);
2014-10-20, by wenzelm
repared document;
2014-10-20, by wenzelm
merged
2014-10-20, by wenzelm
official support for "tt" style variants, avoid fragile \verb in LaTeX;
2014-10-20, by wenzelm
removed dead code;
2014-10-20, by wenzelm
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
2014-10-20, by wenzelm
tweaked
2014-10-20, by paulson
avoid unsafe simp rules
2014-10-20, by haftmann
more standard declaration for presburger
2014-10-20, by haftmann
augmented and tuned facts on even/odd and division
2014-10-20, by haftmann
prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-10-19, by haftmann
NEWS;
2014-10-19, by wenzelm
omit pointless nodes for proof commands etc.;
2014-10-19, by wenzelm
tuned signature and modules;
2014-10-19, by wenzelm
merged
2014-10-18, by wenzelm
NEWS;
2014-10-18, by wenzelm
more folds;
2014-10-18, by wenzelm
always apply precedingFoldLevels, avoid unclear shortcuts;
2014-10-18, by wenzelm
make double-sure that line context is present, e.g. relevant for last line after visible text;
2014-10-18, by wenzelm
clarified Line_Structure wrt. command span;
2014-10-18, by wenzelm
tuned signature;
2014-10-18, by wenzelm
tuned signature;
2014-10-18, by wenzelm
tuned signature;
2014-10-18, by wenzelm
more explicit Line_Nesting;
2014-10-16, by wenzelm
tuned comments;
2014-10-16, by wenzelm
support line context with depth;
2014-10-16, by wenzelm
proper type comparison (amending cd4439d8799c);
2014-10-16, by wenzelm
tuned;
2014-10-16, by wenzelm
tuned
2014-10-16, by haftmann
standard elimination rule for even
2014-10-16, by haftmann
tuned facts on even and power
2014-10-16, by haftmann
restructured
2014-10-16, by haftmann
even more cleanup
2014-10-16, by haftmann
made SML/NJ happier
2014-10-16, by blanchet
made SML/NJ happier
2014-10-15, by blanchet
tuned whitespace
2014-10-15, by blanchet
buffer_line_context via untyped access;
2014-10-14, by wenzelm
access class hierarchy;
2014-10-14, by wenzelm
legacy cleanup
2014-10-14, by haftmann
more algebraic deductions for facts on even/odd
2014-10-14, by haftmann
more algebraic deductions for facts on even/odd
2014-10-14, by haftmann
purely algebraic characterization of even and odd
2014-10-14, by haftmann
document 'sel_transfer'
2014-10-14, by desharna
generate 'sel_transfer' for (co)datatypes
2014-10-14, by desharna
add 'kind' to 'cr_sugar'
2014-10-14, by desharna
add 'fp_bnf' to 'bnf_sugar'
2014-10-14, by desharna
preserve the structure of 'set_intros' theorem in ML
2014-10-14, by desharna
preserve the structure of 'map_sel' theorem in ML
2014-10-14, by desharna
preserve the structure of 'set_sel' theorem in ML
2014-10-14, by desharna
Fixed bug in waldmeister skolemization
2014-10-14, by steckerm
tuned signature;
2014-10-14, by wenzelm
tuned signature;
2014-10-13, by wenzelm
merged
2014-10-13, by wenzelm