2014-07-24 wenzelm 2014-07-24 more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
2014-07-24 wenzelm 2014-07-24 reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
2014-07-24 wenzelm 2014-07-24 tuned;
2014-07-24 wenzelm 2014-07-24 less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
2014-07-24 wenzelm 2014-07-24 updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
2014-07-24 blanchet 2014-07-24 stick to external proofs when invoking E, because they are more detailed and do not merge steps
2014-07-24 blanchet 2014-07-24 more robust handling of types for skolems (modeled as Frees)
2014-07-24 blanchet 2014-07-24 tuning
2014-07-24 blanchet 2014-07-24 repaired named derivations
2014-07-24 blanchet 2014-07-24 use the noted theorems in 'BNF_Comp'
2014-07-24 blanchet 2014-07-24 use the noted theorem whenever possible, also in 'BNF_Def'
2014-07-24 blanchet 2014-07-24 use termtab instead of (perhaps overly sensitive) thmtab
2014-07-24 blanchet 2014-07-24 use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
2014-07-23 wenzelm 2014-07-23 tuned message;
2014-07-23 wenzelm 2014-07-23 added action "isabelle.options" (despite problems with initial window size);
2014-07-23 wenzelm 2014-07-23 more official Thy_Info.script_thy;
2014-07-23 wenzelm 2014-07-23 more frugal edits;
2014-07-23 wenzelm 2014-07-23 enable hires explictly, as seen for other high-end Java applications on the Web;
2014-07-23 wenzelm 2014-07-23 more markup;
2014-07-23 wenzelm 2014-07-23 another attempt at more aggressive auto-loading (amending af28fdd50690) -- hidden buffers are now suppressed;
2014-07-23 wenzelm 2014-07-23 more frugal edits;
2014-07-23 wenzelm 2014-07-23 more explicit treatment of cleared nodes (removal is implicit);
2014-07-23 wenzelm 2014-07-23 clarified display;
2014-07-23 wenzelm 2014-07-23 more workarounds for scalac;
2014-07-23 wenzelm 2014-07-23 clarified display;
2014-07-23 wenzelm 2014-07-23 avoid redundant data structure;
2014-07-23 wenzelm 2014-07-23 more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-07-23 wenzelm 2014-07-23 tuned;
2014-07-23 wenzelm 2014-07-23 tuned comments;
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;