isabelle: Graph

basic support for extended syntax styles: sub/superscript;
2011-06-18, by wenzelm
tuned -- Map.empty serves as partial function;
2011-06-18, by wenzelm
proper place for config files (cf. 55866987a7d9);
2011-06-18, by wenzelm
tuned signature;
2011-06-18, by wenzelm
merged
2011-06-18, by wenzelm
IMP compiler with int, added reverse soundness direction
2011-06-17, by kleing
proper place for config files;
2011-06-18, by wenzelm
tuned markup;
2011-06-18, by wenzelm
highlight via foreground painter, using alpha channel;
2011-06-18, by wenzelm
tuned signature;
2011-06-18, by wenzelm
tuned text;
2011-06-18, by wenzelm
inner literal/delimiter corresponds to outer keyword/operator;
2011-06-18, by wenzelm
tuned markup;
2011-06-18, by wenzelm
more uniform treatment of "keyword" vs. "operator";
2011-06-18, by wenzelm
simplified Line_Context (again);
2011-06-18, by wenzelm
more robust treatment of partial range restriction;
2011-06-18, by wenzelm
select_markup: no filtering here -- results may be distorted anyway;
2011-06-18, by wenzelm
more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;
2011-06-17, by wenzelm
more explicit error message;
2011-06-17, by wenzelm
merged
2011-06-17, by wenzelm
gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"
2011-06-16, by blanchet
added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users
2011-06-16, by blanchet
fixed soundness bug related to extensionality
2011-06-16, by blanchet
unconditional recovery from bad context (e.g. Quoted with malformed quoted_body);
2011-06-17, by wenzelm
flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
2011-06-17, by wenzelm
recovered markup for non-alphabetic keywords;
2011-06-17, by wenzelm
more precise imitation of original TextAreaPainter: no locking;
2011-06-16, by wenzelm
more precise imitatation of original TokenMarker: no locking, interned context etc.;
2011-06-16, by wenzelm
brute-force range restriction to avoid spurious crashes;
2011-06-16, by wenzelm
static token markup, based on outer syntax only;
2011-06-16, by wenzelm
explicit dependency on Pure.jar;
2011-06-16, by wenzelm
partial scans of nested comments;
2011-06-16, by wenzelm
some support for partial scans with explicit context;
2011-06-16, by wenzelm
tuned spelling
2011-06-16, by haftmann
updated generated file;
2011-06-15, by wenzelm
merged
2011-06-15, by wenzelm
spelling
2011-06-15, by haftmann
avoid compiler warning -- this is unchecked anyway;
2011-06-15, by wenzelm
tuned messages;
2011-06-15, by wenzelm
uniform use of Document_View.robust_body;
2011-06-15, by wenzelm
merged
2011-06-15, by wenzelm
merge
2011-06-15, by blanchet
fixed soundness bug made more visible by previous change
2011-06-15, by blanchet
use more appropriate type systems for ATP exporter
2011-06-15, by blanchet
type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases
2011-06-15, by blanchet
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
2011-06-15, by wenzelm
more robust init;
2011-06-15, by wenzelm
recovered orig_text_painter from f4141da52e92;
2011-06-15, by wenzelm
tuned;
2011-06-15, by wenzelm
more elaborate syntax styles;
2011-06-15, by wenzelm
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
2011-06-15, by wenzelm
paint caret according to precise font metrics;
2011-06-15, by wenzelm
include scala mode;
2011-06-14, by wenzelm
builtin sub/superscript styles for jedit-4.3.2;
2011-06-14, by wenzelm
merged
2011-06-14, by wenzelm
tuned colors;
2011-06-14, by wenzelm
recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);
2011-06-14, by wenzelm
more foreground markup, using actual CSS color names;
2011-06-14, by wenzelm
slightly more general treatment of mutually recursive datatypes;
2011-06-14, by boehmes
more explicit check of dependencies;
2011-06-14, by wenzelm
tuned;
2011-06-14, by wenzelm
misc tuning and simplification;
2011-06-14, by wenzelm
separate module for text area painting;
2011-06-14, by wenzelm
improved mutabelle script to use nat for quickcheck_narrowing
2011-06-14, by bulwahn
quickcheck_narrowing returns some timing information
2011-06-14, by bulwahn
removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)
2011-06-14, by bulwahn
more accurate CSS colors;
2011-06-13, by wenzelm
some direct text foreground painting, instead of token marking;
2011-06-13, by wenzelm
imitate original Chunk.paintChunkList;
2011-06-13, by wenzelm
tuned;
2011-06-13, by wenzelm
always use our text painter;
2011-06-13, by wenzelm
use orig_text_painter for extras outside main text (also required to update internal line infos);
2011-06-13, by wenzelm
more precise imitation of original TextAreaPainter$PaintText;
2011-06-12, by wenzelm
tuned;
2011-06-12, by wenzelm
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
2011-06-12, by wenzelm
check source dependencies only if jedit_build component is available;
2011-06-12, by wenzelm
cover method "deepen" concisely;
2011-06-11, by wenzelm
moved/updated single-step tactics;
2011-06-11, by wenzelm
tuned sections;
2011-06-11, by wenzelm
reverted 5fcd0ca1f582 -- isatest provides its own libgmp3 via LD_LIBRARY_PATH, which are also required for swipl;
2011-06-11, by wenzelm
tuned comment
2011-06-11, by haftmann
name tuning
2011-06-10, by blanchet
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
2011-06-10, by blanchet
don't trim proofs in debug mode
2011-06-10, by blanchet
tuning
2011-06-10, by blanchet
isatest/makedist: build Isabelle/jEdit;
2011-06-10, by wenzelm
makedist -j: build Isabelle/jEdit via given jedit_build component;
2011-06-10, by wenzelm
adding another narrowing strategy for integers
2011-06-10, by bulwahn
merged
2011-06-10, by wenzelm
pass --trim option to "eproof" script to speed up proof reconstruction
2011-06-10, by blanchet
removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them
2011-06-10, by blanchet
fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day
2011-06-10, by blanchet
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
2011-06-10, by blanchet
use existing ghc on macbroy20;
2011-06-10, by wenzelm
local gensym based on Name.variant;
2011-06-10, by wenzelm
uniform use of flexflex_rule;
2011-06-10, by wenzelm
tuned name (cf. blast_stats);
2011-06-10, by wenzelm
more official options blast_trace, blast_stats;
2011-06-10, by wenzelm
merged
2011-06-09, by wenzelm
merged
2011-06-09, by bulwahn
resolving an issue with class instances that are pseudo functions in the OCaml code serializer
2011-06-09, by bulwahn
merged
2011-06-09, by hoelzl
fixed document generation for HOL
2011-06-09, by hoelzl
lemma: independence is equal to mutual information = 0
2011-06-09, by hoelzl
jensens inequality
2011-06-09, by hoelzl
lemmas about right derivative and limits
2011-06-09, by hoelzl
lemma about differences of convex functions
2011-06-09, by hoelzl
lemmas relating ln x and x - 1
2011-06-09, by hoelzl
use divide instead of inverse for the derivative of ln
2011-05-31, by hoelzl
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
2011-06-09, by bulwahn
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09, by wenzelm
document depth arguments of method "auto";
2011-06-09, by wenzelm
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
2011-06-09, by wenzelm
clarified special incr_type_indexes;
2011-06-09, by wenzelm
tuned signature: Name.invent and Name.invent_names;
2011-06-09, by wenzelm
modernized structure ProofContext;
2011-06-08, by wenzelm
even more robust \isaspacing;
2011-06-09, by wenzelm
simplified Name.variant -- discontinued builtin fold_map;
2011-06-09, by wenzelm
some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);
2011-06-09, by wenzelm
discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-09, by wenzelm
prefer new-style Name.invents;
2011-06-09, by wenzelm
more tight name invention -- avoiding old functions;
2011-06-09, by wenzelm
\frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;
2011-06-09, by wenzelm
tuned;
2011-06-09, by wenzelm
NEWS
2011-06-09, by bulwahn
correcting import theory of examples
2011-06-09, by bulwahn
fixing code generation test
2011-06-09, by bulwahn
removing char setup
2011-06-09, by bulwahn