2015-04-27 wenzelm 2015-04-27 code equations as displayable content in code dependency graph
2015-04-27 wenzelm 2015-04-27 filtering of reflexive dependencies avoids problems with state-of-the-art graph browser; clarified
2015-04-25 wenzelm 2015-04-25 added checkbox for try0;
2015-04-25 blanchet 2015-04-25 made CVC4 support work also without unsat cores
2015-04-24 wenzelm 2015-04-24 more paranoia settings, e.g. relevant for Ubuntu 15.04;
2015-04-24 wenzelm 2015-04-24 Added tag Isabelle2015-RC2 for changeset 8483c2883c8c
2015-04-24 wenzelm 2015-04-24 always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
2015-04-24 wenzelm 2015-04-24 tuned;
2015-04-24 wenzelm 2015-04-24 tuned message, in accordance to ML side;
2015-04-24 wenzelm 2015-04-24 tuned settings to avoid sporadic crashes;
2015-04-24 wenzelm 2015-04-24 clarified settings for default Poly/ML version: test the actual Isabelle component;
2015-04-22 blanchet 2015-04-22 avoid binding warning in Nitpick
2015-04-22 blanchet 2015-04-22 doc
2015-04-22 wenzelm 2015-04-22 clarified permissions;
2015-04-22 wenzelm 2015-04-22 allow diagnostic proof commands with skip_proofs;
2015-04-22 wenzelm 2015-04-22 tuned signature;
2015-04-22 wenzelm 2015-04-22 updated polyml according to fixes-5.5.2 SVN version 2009;
2015-04-20 blanchet 2015-04-20 declare Nitpick atoms to avoid '??.' prefixes in output
2015-04-19 wenzelm 2015-04-19 proper isatest machine;
2015-05-23 wenzelm 2015-05-23 prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
2015-05-12 nipkow 2015-05-12 this warning is hardly useful but produces noisy markers in the jedit interface
2015-05-09 nipkow 2015-05-09 undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
2015-05-07 hoelzl 2015-05-07 generalized tends over powr; added DERIV rule for powr
2015-05-06 blanchet 2015-05-06 added acknowledgment
2015-05-05 immler 2015-05-05 general Taylor series expansion with integral remainder
2015-05-05 immler 2015-05-05 generalized class constraints
2015-05-05 immler 2015-05-05 generalized differentiable_bound; some further variations of differentiable_bound
2015-05-05 immler 2015-05-05 moved basic lemmas about has_vector_derivative
2015-05-05 immler 2015-05-05 closures of intervals
2015-05-05 hoelzl 2015-05-05 add lfp/gfp rule for nn_integral
2015-05-04 hoelzl 2015-05-04 strengthened lfp_ordinal_induct; added dual gfp variant
2015-05-04 hoelzl 2015-05-04 add rules for least/greatest fixed point calculus
2015-05-04 hoelzl 2015-05-04 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2015-05-04 nipkow 2015-05-04 no more simp_legacy_precond
2015-05-04 nipkow 2015-05-04 no longer needed
2015-05-03 nipkow 2015-05-03 swap False to the right in assumptions to be eliminated at the right end
2015-05-01 nipkow 2015-05-01 merged
2015-05-01 nipkow 2015-05-01 simplified statement and proof
2015-05-01 wenzelm 2015-05-01 tuned spelling;
2015-05-01 paulson 2015-05-01 Merge
2015-04-30 paulson 2015-04-30 Merge
2015-04-30 paulson 2015-04-30 Merge
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-05-01 nipkow 2015-05-01 new simp rule
2015-04-30 wenzelm 2015-04-30 more formal source, more PIDE markup;
2015-04-30 wenzelm 2015-04-30 tuned -- avoid odd rebinding of "ctxt" and "context";
2015-04-30 wenzelm 2015-04-30 tuned;
2015-04-29 wenzelm 2015-04-29 use smaller example that fits into 64MB string limit of Poly/ML x86 platform;
2015-04-29 wenzelm 2015-04-29 tuned;
2015-04-29 paulson 2015-04-29 Tidying. Improved simplification for numerals, esp in exponents.
2015-04-28 blanchet 2015-04-28 allow sorts on dead variables in BNFs
2015-04-28 blanchet 2015-04-28 added known bug
2015-04-28 blanchet 2015-04-28 tuning
2015-04-28 nipkow 2015-04-28 undid 6d7b7a037e8d
2015-04-28 paulson 2015-04-28 New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-04-28 paulson 2015-04-28 Fixed a non-terminating proof (almost certainly caused by no change of mind)
2015-04-27 nipkow 2015-04-27 new lemma
2015-04-25 nipkow 2015-04-25 new ==> simp rule
2015-04-22 blanchet 2015-04-22 improved docs
2015-04-22 nipkow 2015-04-22 merged