2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-07-23 wenzelm 2014-07-23 proper change of perspective for removed nodes (stemming from closed buffers);
2014-07-23 wenzelm 2014-07-23 tuned signature;
2014-07-22 wenzelm 2014-07-22 some robustification of console output;
2014-07-22 wenzelm 2014-07-22 updated ErrorList.jar;
2014-07-22 wenzelm 2014-07-22 discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;
2014-07-22 wenzelm 2014-07-22 evade problems with MikTeX on Windows;
2014-07-22 wenzelm 2014-07-22 tuned messages;
2014-07-22 wenzelm 2014-07-22 support multiple selected print operations instead of slightly odd "menu";
2014-07-22 wenzelm 2014-07-22 more default imports;
2014-07-22 wenzelm 2014-07-22 no keyword completion within word context -- especially avoid its odd visual rendering;
2014-07-22 Andreas Lochbihler 2014-07-22 merged
2014-07-21 Andreas Lochbihler 2014-07-21 merged
2014-07-21 Andreas Lochbihler 2014-07-21 add parametricity lemmas
2014-07-21 Andreas Lochbihler 2014-07-21 add lemma
2014-07-21 wenzelm 2014-07-21 merged
2014-07-21 wenzelm 2014-07-21 refer to Simplifier Trace panel on first invocation;
2014-07-21 wenzelm 2014-07-21 removed unused markup (cf. 2f7d91242b99);
2014-07-21 wenzelm 2014-07-21 regular message to refer to Simplifier Trace panel (unused);
2014-07-21 wenzelm 2014-07-21 proper Swing buttons instead of active areas within text (by Lars Hupel);
2014-07-21 wenzelm 2014-07-21 misc tuning and simplification;
2014-07-21 wenzelm 2014-07-21 clarified "simp_trace_new" and corresponding isar-ref section;
2014-07-21 wenzelm 2014-07-21 more on "Simplifier trace" (by Lars Hupel);
2014-07-21 wenzelm 2014-07-21 always complete explicit symbols;
2014-07-21 wenzelm 2014-07-21 discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
2014-07-21 wenzelm 2014-07-21 updated to jdk-7u65;
2014-07-21 traytel 2014-07-21 regression test for datatypes defined in IsaFoR
2014-07-21 kleing 2014-07-21 ghc mac installation repaired; test back on.
2014-07-20 wenzelm 2014-07-20 proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
2014-07-20 wenzelm 2014-07-20 updated to jdk-8u11 (inactive);
2014-07-20 wenzelm 2014-07-20 avoid delay_load overrun;
2014-07-20 wenzelm 2014-07-20 provide explicit options file -- avoid multiple Scala/JVM invocation;
2014-07-20 wenzelm 2014-07-20 check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
2014-07-19 kleing 2014-07-19 attempt to run without ISABELLE_GHC setting again on mac-poly
2014-07-19 kleing 2014-07-19 apparently, setting ISABELLE_GHC makes ghc unusable
2014-07-19 haftmann 2014-07-19 reverse induction over nonempty lists
2014-07-19 haftmann 2014-07-19 more appropriate postprocessing of rational numbers: extract sign to front of fraction
2014-07-19 blanchet 2014-07-19 doc fixes (contributed by Christian Sternagel)
2014-07-19 blanchet 2014-07-19 made SML/NJ happier
2014-07-18 kleing 2014-07-18 avoid duplicate fact name
2014-07-18 kleing 2014-07-18 afp-poly runs on macbroy2 (different ghc)
2014-07-18 nipkow 2014-07-18 reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
2014-07-18 nipkow 2014-07-18 tuned
2014-07-17 hoelzl 2014-07-17 register tree with datatype_compat ot support QuickCheck
2014-07-17 desharna 2014-07-17 fix bug caused by bad context
2014-07-17 desharna 2014-07-17 add mk_Trueprop_mem utility function
2014-07-16 blanchet 2014-07-16 disabled MaSh for the Isabelle2014 release, due to a couple of issues
2014-07-16 desharna 2014-07-16 refactor commonly used functions
2014-07-16 desharna 2014-07-16 document property 'rel_sel'
2014-07-16 desharna 2014-07-16 generate 'rel_sel' theorem for (co)datatypes
2014-07-16 desharna 2014-07-16 fix rel_cases
2014-07-15 blanchet 2014-07-15 made SML/NJ happier
2014-07-15 kleing 2014-07-15 add ISABELLE_GHC settings for isatest
2014-07-14 noschinl 2014-07-14 mira.py: building jEdit plugin is required for makeall
2014-07-15 blanchet 2014-07-15 took out 'rel_cases' for now because of failing tactic
2014-07-15 blanchet 2014-07-15 record MaSh algorithm in spying data
2014-07-15 blanchet 2014-07-15 tuned whitespace (also in strings)
2014-07-15 blanchet 2014-07-15 also learn when 'fact_filter =' is set explicitly
2014-07-15 blanchet 2014-07-15 no warning in case MaSh is disabled
2014-07-15 blanchet 2014-07-15 don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic