2016-03-17 wenzelm 2016-03-17 @{make_string} is available during Pure bootstrap;
2016-03-17 wenzelm 2016-03-17 clarified modules;
2016-03-17 wenzelm 2016-03-17 unused;
2016-03-17 wenzelm 2016-03-17 hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
2016-03-17 wenzelm 2016-03-17 obsolete;
2016-03-17 wenzelm 2016-03-17 tuned signature;
2016-03-17 wenzelm 2016-03-17 obsolete;
2016-03-17 wenzelm 2016-03-17 tuned whitespace;
2016-03-17 wenzelm 2016-03-17 proper ML type;
2016-03-18 Andreas Lochbihler 2016-03-18 merged
2016-03-18 Andreas Lochbihler 2016-03-18 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-18 nipkow 2016-03-18 superfluous premise (noticed by Julian Nagele)
2016-03-18 nipkow 2016-03-18 added tree lemmas
2016-03-18 traytel 2016-03-18 normalize schematic names since they are used to instantiate the theorem later
2016-03-17 hoelzl 2016-03-17 more stuff for extended nonnegative real numbers
2016-03-17 Andreas Lochbihler 2016-03-17 less preconditions
2016-03-16 wenzelm 2016-03-16 merged
2016-03-16 wenzelm 2016-03-16 eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
2016-03-16 wenzelm 2016-03-16 pro-forma selection for improved error message;
2016-03-16 wenzelm 2016-03-16 eliminated without magic name;
2016-03-16 wenzelm 2016-03-16 NEWS;
2016-03-16 wenzelm 2016-03-16 always build with full results; always print unfinished sessions;
2016-03-16 wenzelm 2016-03-16 clarified name;
2016-03-16 wenzelm 2016-03-16 isabelle process -d; proper args;
2016-03-16 wenzelm 2016-03-16 tuned signature;
2016-03-16 wenzelm 2016-03-16 support for Poly/ML heap hierarchy, which saves a lot of disk space;
2016-03-16 wenzelm 2016-03-16 clarified signature;
2016-03-16 wenzelm 2016-03-16 tuned signature;
2016-03-16 wenzelm 2016-03-16 less physical "logic" argument, with option -l like "isabelle console" etc.;
2016-03-15 wenzelm 2016-03-15 find heaps uniformly via Sessions.Store; tuned;
2016-03-15 wenzelm 2016-03-15 clarified modules;
2016-03-15 wenzelm 2016-03-15 clarified modules;
2016-03-15 wenzelm 2016-03-15 ML save_state under control of Isabelle/Scala;
2016-03-15 wenzelm 2016-03-15 clarified prompt: "ML" usually means Isabelle/ML;
2016-03-14 wenzelm 2016-03-14 record stamps of cumulative input heaps; tuned;
2016-03-16 paulson 2016-03-16 Merge
2016-03-16 paulson 2016-03-16 Contractible sets. Also removal of obsolete theorems and refactoring
2016-03-16 hoelzl 2016-03-16 add measurability rules for ennreal
2016-03-16 hoelzl 2016-03-16 generalized some Borel measurable statements to support ennreal
2016-03-15 paulson 2016-03-15 rationalisation of theorem names esp about "real Archimedian" etc.
2016-03-15 Andreas Lochbihler 2016-03-15 add fixpoint induction principle
2016-03-14 blanchet 2016-03-14 generalized ML function
2016-03-14 paulson 2016-03-14 New results about paths, segments, etc. The notion of simply_connected.
2016-03-14 paulson 2016-03-14 Merge
2016-03-14 paulson 2016-03-14 Refactoring (moving theorems into better locations), plus a bit of new material
2016-03-14 blanchet 2016-03-14 strengthened tactics
2016-03-13 wenzelm 2016-03-13 tuned;
2016-03-13 wenzelm 2016-03-13 tuned signature;
2016-03-13 wenzelm 2016-03-13 prefer Scala over bash function;
2016-03-13 wenzelm 2016-03-13 tuned;
2016-03-13 wenzelm 2016-03-13 clarified env;
2016-03-13 wenzelm 2016-03-13 unused;
2016-03-13 wenzelm 2016-03-13 more uniform signature for various process invocations; env refers to full environment, not the update;
2016-03-13 wenzelm 2016-03-13 tuned;
2016-03-13 haftmann 2016-03-13 more theorems on orderings
2016-03-13 haftmann 2016-03-13 dropped junk
2016-03-12 wenzelm 2016-03-12 tuned;
2016-03-12 wenzelm 2016-03-12 merged
2016-03-12 wenzelm 2016-03-12 tuned;
2016-03-12 wenzelm 2016-03-12 clarified cleanup;