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;
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