tuned colors;

recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);

more foreground markup, using actual CSS color names;

slightly more general treatment of mutually recursive datatypes; treat datatype constructors and selectors similarly to built-in constants wrt. introduction of explicit application (in the same way as what is already done for eta-expansion)

more explicit check of dependencies;

tuned;

misc tuning and simplification;

separate module for text area painting;

improved mutabelle script to use nat for quickcheck_narrowing

quickcheck_narrowing returns some timing information

removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)

more accurate CSS colors;

some direct text foreground painting, instead of token marking; common snapshot for all text area painters (NOT gutter etc.) tuned;

imitate original Chunk.paintChunkList;

tuned;

always use our text painter;

use orig_text_painter for extras outside main text (also required to update internal line infos); tuned;

more precise imitation of original TextAreaPainter$PaintText;

tuned;

separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;

check source dependencies only if jedit_build component is available;

cover method "deepen" concisely;

moved/updated single-step tactics;

tuned sections;

reverted 5fcd0ca1f582 -- isatest provides its own libgmp3 via LD_LIBRARY_PATH, which are also required for swipl;

tuned comment

name tuning

revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug

don't trim proofs in debug mode

tuning

isatest/makedist: build Isabelle/jEdit;

makedist -j: build Isabelle/jEdit via given jedit_build component;

adding another narrowing strategy for integers

merged

pass --trim option to "eproof" script to speed up proof reconstruction

removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them

fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day

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

use existing ghc on macbroy20;

local gensym based on Name.variant; do not export internals by default;

uniform use of flexflex_rule;

tuned name (cf. blast_stats);

more official options blast_trace, blast_stats;

merged

merged

resolving an issue with class instances that are pseudo functions in the OCaml code serializer

merged

fixed document generation for HOL

lemma: independence is equal to mutual information = 0

jensens inequality

lemmas about right derivative and limits

lemma about differences of convex functions

lemmas relating ln x and x - 1

use divide instead of inverse for the derivative of ln

adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10

renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;

document depth arguments of method "auto";

clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b); uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac; tuned blast_tac: atomize prems only once, outside DEEPEN;

clarified special incr_type_indexes;

tuned signature: Name.invent and Name.invent_names;

modernized structure ProofContext;

even more robust \isaspacing;

simplified Name.variant -- discontinued builtin fold_map;

some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);

discontinued Name.variant to emphasize that this is old-style / indirect;

prefer new-style Name.invents;

more tight name invention -- avoiding old functions;

\frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;

tuned;

NEWS

correcting import theory of examples

fixing code generation test

removing char setup

removing unneccessary manual instantiations and dead definitions; hiding more constants and facts

adding a nicer error message for quickcheck_narrowing; hiding fact empty_def

adding narrowing engine for existentials

adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement

adding theory Quickcheck_Narrowing to HOL-Main image

adapting IsaMakefile

moving Quickcheck_Narrowing from Library to base directory

compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators

local simp rule in List_Cset

tuning

compile

cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)

added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)

improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well

removed needless function that duplicated standard functionality, with a little unnecessary twist

removed more dead code

be a bit more liberal with respect to the universal sort -- it sometimes help

renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"

merged

avoid duplicate facts, which confuse the minimizer output

pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types

restore comment about subtle issue

made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded