isabelle: Graph

fragment of a HOL type class primer
2016-04-18, by haftmann
capitalized GCD and LCM syntax
2016-04-18, by haftmann
environment variable check has become pointless after 771b8ad5c7fc
2016-04-18, by haftmann
unfold internal definitions before emitting a proof obligation
2016-04-19, by traytel
more IDE support for Isabelle/Pure bootstrap;
2016-04-19, by wenzelm
merged
2016-04-18, by wenzelm
tuned signature;
2016-04-18, by wenzelm
prefer internal attribute source;
2016-04-18, by wenzelm
tidying some proofs; getting rid of "nonempty_witness"
2016-04-18, by paulson
Merge
2016-04-18, by paulson
numerous theorems about affine hulls, hyperplanes, etc.
2016-04-18, by paulson
merged
2016-04-18, by wenzelm
proper LaTeX;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
clarified bindings;
2016-04-18, by wenzelm
clarified bindings;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
avoid clash with function called "x";
2016-04-18, by wenzelm
new theorems about convex hulls, etc.; also, renamed some theorems
2016-04-18, by paulson
clarified bindings;
2016-04-17, by wenzelm
clarified bindings;
2016-04-17, by wenzelm
prefer binding over base name;
2016-04-17, by wenzelm
clarified signature;
2016-04-17, by wenzelm
removed pointless check (see Type_Infer.object_logic);
2016-04-17, by wenzelm
prefer precise names for internal construction;
2016-04-17, by wenzelm
remove "slow" session tags
2016-04-17, by Lars Hupel
misc tuning and modernization;
2016-04-17, by wenzelm
clarified reported positions;
2016-04-17, by wenzelm
operate on proper binding;
2016-04-17, by wenzelm
tuned;
2016-04-17, by wenzelm
add "slow" group to descendants of HOL-Proofs
2016-04-15, by Lars Hupel
merged
2016-04-15, by wenzelm
support for Poly/ML entity ids;
2016-04-15, by wenzelm
clarified PIDE reports;
2016-04-15, by wenzelm
clarified rendering wrt. hyperlinks;
2016-04-15, by wenzelm
tuned -- no position;
2016-04-15, by wenzelm
clarified focus visibility;
2016-04-15, by wenzelm
tuned rendering;
2016-04-15, by wenzelm
highlighting of entity def/ref positions wrt. cursor;
2016-04-14, by wenzelm
background color for entity def/ref focus;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
more silence;
2016-04-14, by wenzelm
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
clarified context;
2016-04-14, by wenzelm
misc tuning and standardization;
2016-04-14, by wenzelm
tuned headers;
2016-04-14, by wenzelm
fix HOL-Probability-ex
2016-04-15, by hoelzl
change is incompatible
2016-04-14, by hoelzl
Probability: move emeasure and nn_integral from ereal to ennreal
2016-04-14, by hoelzl
tuned;
2016-04-14, by wenzelm
clarified modules;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
back to exact copy of non-text file (amending dcc8e1d34b18);
2016-04-14, by wenzelm
merged
2016-04-13, by wenzelm
eliminated "xname" and variants;
2016-04-13, by wenzelm
clarified syntax;
2016-04-13, by wenzelm
more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
2016-04-13, by wenzelm
tuned;
2016-04-13, by wenzelm
clarified syntax;
2016-04-13, by wenzelm
avoid quotes for qualified names;
2016-04-13, by wenzelm
added rule
2016-04-13, by immler
tuned;
2016-04-12, by wenzelm
merged
2016-04-12, by wenzelm
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
2016-04-12, by wenzelm
back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff);
2016-04-12, by wenzelm
Type_Infer.object_logic controls improvement of type inference result;
2016-04-12, by wenzelm
tuned;
2016-04-12, by wenzelm
simplified constraints;
2016-04-11, by wenzelm
back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;
2016-04-11, by wenzelm
tuned imports;
2016-04-11, by wenzelm
tuned message;
2016-04-11, by wenzelm
tuned;
2016-04-11, by wenzelm
added lemmas
2016-04-12, by immler
generalized
2016-04-12, by immler
added derivative of scaling in exponential function
2016-04-12, by immler
lots of new theorems for multivariate analysis
2016-04-11, by paulson
tuned;
2016-04-10, by wenzelm
tuned;
2016-04-10, by wenzelm
tuned comments;
2016-04-10, by wenzelm
more standard session build process, including browser_info;
2016-04-10, by wenzelm
clarified files;
2016-04-10, by wenzelm
tuned;
2016-04-10, by wenzelm
proper support for recursive ML debugging;
2016-04-10, by wenzelm
tuned -- avoid recoding properties;
2016-04-10, by wenzelm
removed old proof method "default";
2016-04-09, by wenzelm
clean message more thoroughly;
2016-04-09, by wenzelm
clarified modules;
2016-04-09, by wenzelm
avoid interference with running PIDE protocol;
2016-04-09, by wenzelm
proper signature for structure;
2016-04-09, by wenzelm
tuned signature;
2016-04-09, by wenzelm
proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
2016-04-09, by wenzelm
support ROOT0.ML as well -- independently of ROOT.ML;
2016-04-09, by wenzelm
flags as in 'ML' command;
2016-04-09, by wenzelm
shared output primitives of physical/virtual Pure;
2016-04-09, by wenzelm
shared thread position for physical/virtual Pure;
2016-04-09, by wenzelm
prefer Synchronized.var;
2016-04-09, by wenzelm
tuned signature;
2016-04-09, by wenzelm
virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
2016-04-09, by wenzelm
tuned signature;
2016-04-09, by wenzelm
tuned signature -- closer to Exn.Interrupt.expose in Scala;
2016-04-09, by wenzelm
clarified bootstrap;
2016-04-09, by wenzelm
clarified context;
2016-04-09, by wenzelm
old;
2016-04-09, by wenzelm
ensure globally unique counter results;
2016-04-09, by wenzelm
tuned;
2016-04-09, by wenzelm
clarified modules;
2016-04-09, by wenzelm
backout 930a30c1a9af: leads to odd effect of command-line options becoming persistent preferences;
2016-04-08, by wenzelm
eliminated ancient TTY-based Tactical.tracify and related global references;
2016-04-08, by wenzelm
updated according to 705d4c4003ea;
2016-04-08, by wenzelm
option "-o" for "isabelle jedit";
2016-04-08, by wenzelm
eliminated unused simproc identifier;
2016-04-08, by wenzelm
section headings for ROOT.ML;
2016-04-07, by wenzelm
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
2016-04-07, by wenzelm
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
2016-04-07, by wenzelm
clarified word syntax: "." is separator or delimiter;
2016-04-07, by wenzelm
clarified mode of ROOT.ML files;
2016-04-07, by wenzelm
(un)folds are not legacy
2016-04-07, by traytel
removed duplicate lemma
2016-04-07, by traytel
derive (co)rec uniformly from (un)fold
2016-04-07, by traytel
NEWS;
2016-04-07, by wenzelm
updated documentation;
2016-04-07, by wenzelm
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
2016-04-07, by wenzelm
unused (see caaa2fc4040d);
2016-04-07, by wenzelm
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
2016-04-07, by wenzelm
clarified bootstrap of @{make_string} -- avoid query on ML environment;
2016-04-07, by wenzelm
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
2016-04-07, by wenzelm
prefer regular context update, to allow continuous editing of Pure;
2016-04-07, by wenzelm
clarified editor mode;
2016-04-07, by wenzelm
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-06, by wenzelm
more robust bootstrap;
2016-04-06, by wenzelm
virtual thread data via context, for proper support of Context.>> etc;
2016-04-06, by wenzelm
unused;
2016-04-06, by wenzelm
tuned signature;
2016-04-06, by wenzelm
clarified bootstrap;
2016-04-06, by wenzelm
clarified modules;
2016-04-06, by wenzelm
proper return code;
2016-04-06, by wenzelm
clarified ML bootstrap environment;
2016-04-06, by wenzelm
simplified bootstrap: critical structures remain accessible in ML_Root context;
2016-04-06, by wenzelm
more uniform cleanup (via ML_Process in Scala);
2016-04-06, by wenzelm
clarified bootstrap;
2016-04-06, by wenzelm
clarified ML bootstrap;
2016-04-06, by wenzelm
merged
2016-04-05, by wenzelm
proper file extension;
2016-04-05, by wenzelm
clarified files;
2016-04-05, by wenzelm
back to static conditional compilation -- simplified bootstrap;
2016-04-05, by wenzelm
clarified modules -- simplified bootstrap;
2016-04-05, by wenzelm
avoid malformed Isabelle symbols during bootstrap;
2016-04-05, by wenzelm
clarified modules -- simplified bootstrap;
2016-04-05, by wenzelm
clarified bootstrap environment;
2016-04-05, by wenzelm
actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;
2016-04-05, by wenzelm
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
2016-04-05, by wenzelm
tuned;
2016-04-05, by wenzelm
proper syntax;
2016-04-05, by wenzelm
prefer antiquotations;
2016-04-05, by wenzelm
proper use_thy;
2016-04-05, by wenzelm
support for ML project ROOT file, with imitation of ML "use" commands;
2016-04-05, by wenzelm
tuned;
2016-04-05, by wenzelm
read Pure file dependencies directly from ROOT.ML;
2016-04-05, by wenzelm
tuned output;
2016-04-05, by wenzelm
tuned;
2016-04-05, by wenzelm
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
2016-04-05, by traytel
more uniform ML file commands;
2016-04-04, by wenzelm
tuned;
2016-04-04, by wenzelm
tuned;
2016-04-04, by wenzelm
tuned whitespace;
2016-04-04, by wenzelm
tuned headers;
2016-04-04, by wenzelm
merged
2016-04-04, by wenzelm
tuned -- more explicit sections;
2016-04-04, by wenzelm
clarified bootstrap -- avoid conditional compilation in ROOT.ML;
2016-04-04, by wenzelm
allow empty string;
2016-04-04, by wenzelm
tuned;
2016-04-04, by wenzelm
clarified modules;
2016-04-04, by wenzelm
option ML_system_unsafe;
2016-04-04, by wenzelm
clarified conditional compilation;
2016-04-04, by wenzelm
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
2016-04-04, by wenzelm
clarified bootstrap -- more uniform use of ML files;
2016-04-04, by wenzelm
clarified bootstrap;
2016-04-04, by wenzelm
clarified final setup of ML environment;
2016-04-04, by wenzelm
clarified modules;
2016-04-04, by wenzelm
avoid duplicate reports;
2016-04-04, by wenzelm
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
2016-04-04, by paulson
added reference from NEWS to docs
2016-04-04, by blanchet
merged
2016-04-03, by wenzelm
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
2016-04-03, by wenzelm
clarified SML name space: no access to structure PolyML;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
isabelle update_cartouches -c -t;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
support for internal tools;
2016-04-03, by wenzelm
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
2016-04-03, by wenzelm
clarified usage;
2016-04-03, by wenzelm
tuned names
2016-04-03, by traytel
prefer infix operations;
2016-04-02, by wenzelm
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
2016-04-02, by wenzelm
proper signature;
2016-04-02, by wenzelm
tuned signature;
2016-04-02, by wenzelm
tuned;
2016-04-02, by wenzelm
tuned signature;
2016-04-02, by wenzelm
proper type;
2016-04-02, by wenzelm
careful export of type-dependent functions, without losing their special status;
2016-04-02, by wenzelm
clarified modules;
2016-04-02, by wenzelm
clarified modules;
2016-04-02, by wenzelm
tuned LaTeX
2016-04-02, by blanchet
import package that might help on some machines (e.g., macbroy2)
2016-04-02, by blanchet
clarified check_sources;
2016-04-02, by wenzelm
obsolete (see 1d977436c1bf);
2016-04-02, by wenzelm
more robust display of bidirectional Unicode text: enforce left-to-right;
2016-04-02, by wenzelm
merged
2016-04-01, by wenzelm
merged
2016-04-01, by wenzelm
explicit warning about bidi uncertainty in Unicode;
2016-04-01, by wenzelm
explicit warning about formal use of Unicode;
2016-04-01, by wenzelm
documentation;
2016-04-01, by wenzelm
more markup;
2016-04-01, by wenzelm
require actual space;
2016-04-01, by wenzelm
tuned signature;
2016-04-01, by wenzelm
required space is already part of Position.here;
2016-04-01, by wenzelm
tuned messages;
2016-04-01, by wenzelm
clarified errors -- disallow cartouche fragments as delimiter;
2016-04-01, by wenzelm
tuned signature;
2016-04-01, by wenzelm
tuned;
2016-04-01, by wenzelm
clarified end position;
2016-04-01, by wenzelm
tuned signature;
2016-04-01, by wenzelm
tuned;
2016-04-01, by wenzelm
removed redundant Position.set_range -- already done in Position.range;
2016-04-01, by wenzelm
lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
2016-04-01, by wenzelm
less bulky timing information, e.g. HOL 56913 ~> 672;
2016-04-01, by wenzelm
tuned;
2016-04-01, by wenzelm
more operations (cf. Scala version);
2016-04-01, by wenzelm
tuned whitespace;
2016-04-01, by wenzelm
explicit property for unbreakable block;
2016-04-01, by wenzelm
unused;
2016-04-01, by wenzelm
tuned markup;
2016-04-01, by wenzelm
clarified treatment of properties;
2016-04-01, by wenzelm
more robust pretty printing: permissive treatment of bad values;
2016-04-01, by wenzelm
adapted to Poly/ML repository version 2e40cadc975a;
2016-04-01, by wenzelm
explicit mixfix block properties;
2016-03-31, by wenzelm
clarified modules;
2016-03-31, by wenzelm
tuned signature;
2016-03-31, by wenzelm
reintroduced check that may guard some tactic failures
2016-04-01, by blanchet
adapt theory names within the theory
2016-04-01, by blanchet
made tactic more robust
2016-03-31, by traytel
tuned interface
2016-03-31, by traytel
merged
2016-03-30, by wenzelm
proper object-logic constraint (amending dd2914250ca7);
2016-03-30, by wenzelm
reconcile object-logic constraint vs. mixfix constraint;
2016-03-30, by wenzelm
more explicit support for object-logic constraint;
2016-03-30, by wenzelm
more language markup;
2016-03-30, by wenzelm
more accurate mixfix type constraints;
2016-03-30, by wenzelm
tuned;
2016-03-30, by wenzelm
tuned message;
2016-03-30, by wenzelm
more explicit type;
2016-03-30, by wenzelm
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
2016-03-30, by wenzelm
avoid duplicate reports;
2016-03-30, by wenzelm
tuned messages -- position is usually missing here;
2016-03-30, by wenzelm
more PIDE markup;
2016-03-30, by wenzelm
clarified modules;
2016-03-30, by wenzelm
clarified errors: more positions;
2016-03-30, by wenzelm
clarified simple mixfix;
2016-03-30, by wenzelm
tuned;
2016-03-30, by wenzelm
more operations;
2016-03-30, by wenzelm
updated dependencies;
2016-03-30, by wenzelm
updated to Navigator 2.6;
2016-03-30, by wenzelm
more 'corec' docs
2016-03-30, by blanchet
merged
2016-03-29, by wenzelm
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
2016-03-29, by wenzelm
tuned messages -- more positions;
2016-03-29, by wenzelm
more position information for type mixfix;
2016-03-29, by wenzelm
tuned signature;
2016-03-29, by wenzelm
proper norm_props, e.g. relevant for ML pp;
2016-03-29, by wenzelm
clarified reports;
2016-03-29, by wenzelm
tuned signature;
2016-03-29, by wenzelm
more 'corec' docs
2016-03-29, by blanchet
tuning
2016-03-29, by blanchet
more 'corec' docs
2016-03-29, by blanchet
try tactics in right order w.r.t. schematics
2016-03-29, by blanchet
more natural order for 'cong_intros'
2016-03-29, by blanchet
more 'corec' documentation
2016-03-29, by blanchet
renamed generated theorem
2016-03-29, by blanchet
tuning
2016-03-29, by blanchet
added sketchy 'corec' documentation
2016-03-29, by blanchet
compile
2016-03-28, by blanchet
updated Sledgehammer documentation
2016-03-28, by blanchet
a more generous hard timeout
2016-03-28, by blanchet
early warning when Sledgehammer finds a proof
2016-03-28, by blanchet
another 'corec' example
2016-03-28, by blanchet
don't ask too much of 'transfer_prover'
2016-03-28, by blanchet
commented out for now
2016-03-28, by blanchet
tuning
2016-03-28, by blanchet
FIXME
2016-03-28, by blanchet
avoid 'prove_sorry' for unreliable tactics
2016-03-28, by blanchet
reused code
2016-03-28, by blanchet
tuning
2016-03-28, by blanchet
tuned examples
2016-03-28, by blanchet
new 'corec' example
2016-03-28, by blanchet
more reliable check for rhs variables
2016-03-28, by blanchet
strengthened tactic
2016-03-28, by blanchet
generalized ML function
2016-03-28, by blanchet
added '_legacy' suffixes
2016-03-28, by blanchet
generalized ML interface
2016-03-28, by blanchet
tuning
2016-03-28, by blanchet
refined experimental option of Sledgehammer
2016-03-28, by blanchet
tuned;
2016-03-26, by wenzelm
explicit print_depth for the sake of Spec_Check.determine_type;
2016-03-26, by wenzelm
obsolete -- done in Isabelle_Process.init_options;
2016-03-26, by wenzelm
clarified use of options;
2016-03-26, by wenzelm
tuned signature;
2016-03-26, by wenzelm
clarified use of options;
2016-03-26, by wenzelm
avoid hardwired values;
2016-03-26, by wenzelm
eliminated duplicate;
2016-03-26, by wenzelm
more operations;
2016-03-26, by wenzelm
merged
2016-03-24, by nipkow
merged
2016-03-24, by nipkow
added Leftist_Heap
2016-03-24, by nipkow
updated to scala-2.11.8;
2016-03-24, by wenzelm
proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
2016-03-24, by wenzelm
more operations;
2016-03-24, by wenzelm
tuned signature;
2016-03-24, by wenzelm
HOL-Word: add stronger bl_to_bin_lt2p_drop
2016-03-23, by kleing
proper sectioning
2016-03-23, by blanchet
sorted out type issue with sort constraints
2016-03-23, by blanchet
tuned whitespace
2016-03-22, by blanchet
compile
2016-03-22, by blanchet
added 'corec' examples and tests
2016-03-22, by blanchet
file header
2016-03-22, by blanchet
added two 'corec' examples
2016-03-22, by blanchet
document addition of 'corec'
2016-03-22, by blanchet
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
2016-03-22, by blanchet
put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
2016-03-22, by blanchet
nicer error
2016-03-22, by blanchet
more debugging
2016-03-22, by blanchet
more general, reliable N2M
2016-03-22, by blanchet
better warning, with definitions in right order
2016-03-22, by blanchet
export ML function
2016-03-22, by blanchet
added timers to N2M
2016-03-22, by blanchet
document that n2m does not depend on most things in fp_sugar in its type
2016-03-22, by traytel
clarified rule structure;
2016-03-21, by wenzelm
accomodate Isabelle identifiers with subscripts;
2016-03-21, by wenzelm
more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
2016-03-21, by wenzelm
eliminated unused argument (see also 58110c1e02bc);
2016-03-21, by wenzelm
add le_log_of_power and le_log2_of_power by Tobias Nipkow
2016-03-21, by hoelzl
unified CHAR with CHR syntax
2016-03-19, by haftmann
isabelle process -T THEORY;
2016-03-18, by wenzelm
proper option -l;
2016-03-18, by wenzelm
avoid redundant addLeftOfScrollBar;
2016-03-18, by wenzelm
no dependency on HighlightPlugin, despite e7b2cfcef94c;
2016-03-18, by wenzelm
observe ML print depth;
2016-03-18, by wenzelm
clarified print depth;
2016-03-18, by wenzelm
recovered from Unicode accident in 7248d106c607;
2016-03-18, by wenzelm
merged
2016-03-18, by wenzelm
tuned -- fewer warnings;
2016-03-18, by wenzelm
discontinued slightly odd "secure" mode;
2016-03-18, by wenzelm
clarified Pretty.T toplevel pp;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
tuned header;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
@{make_string} is available during Pure bootstrap;
2016-03-17, by wenzelm
clarified modules;
2016-03-17, by wenzelm
unused;
2016-03-17, by wenzelm
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
2016-03-17, by wenzelm
obsolete;
2016-03-17, by wenzelm
tuned signature;
2016-03-17, by wenzelm
obsolete;
2016-03-17, by wenzelm
tuned whitespace;
2016-03-17, by wenzelm
proper ML type;
2016-03-17, by wenzelm
merged
2016-03-18, by Andreas Lochbihler
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-18, by Andreas Lochbihler
superfluous premise (noticed by Julian Nagele)
2016-03-18, by nipkow
added tree lemmas
2016-03-18, by nipkow
normalize schematic names since they are used to instantiate the theorem later
2016-03-18, by traytel
more stuff for extended nonnegative real numbers
2016-03-17, by hoelzl
less preconditions
2016-03-17, by Andreas Lochbihler
merged
2016-03-16, by wenzelm
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
2016-03-16, by wenzelm
pro-forma selection for improved error message;
2016-03-16, by wenzelm
eliminated without magic name;
2016-03-16, by wenzelm
NEWS;
2016-03-16, by wenzelm
always build with full results;
2016-03-16, by wenzelm
clarified name;
2016-03-16, by wenzelm
isabelle process -d;
2016-03-16, by wenzelm
tuned signature;
2016-03-16, by wenzelm
support for Poly/ML heap hierarchy, which saves a lot of disk space;
2016-03-16, by wenzelm
clarified signature;
2016-03-16, by wenzelm
tuned signature;
2016-03-16, by wenzelm
less physical "logic" argument, with option -l like "isabelle console" etc.;
2016-03-16, by wenzelm
find heaps uniformly via Sessions.Store;
2016-03-15, by wenzelm
clarified modules;
2016-03-15, by wenzelm
clarified modules;
2016-03-15, by wenzelm
ML save_state under control of Isabelle/Scala;
2016-03-15, by wenzelm
clarified prompt: "ML" usually means Isabelle/ML;
2016-03-15, by wenzelm
record stamps of cumulative input heaps;
2016-03-14, by wenzelm
Merge
2016-03-16, by paulson
Contractible sets. Also removal of obsolete theorems and refactoring
2016-03-16, by paulson
add measurability rules for ennreal
2016-03-16, by hoelzl
generalized some Borel measurable statements to support ennreal
2016-03-16, by hoelzl
rationalisation of theorem names esp about "real Archimedian" etc.
2016-03-15, by paulson
add fixpoint induction principle
2016-03-15, by Andreas Lochbihler
generalized ML function
2016-03-14, by blanchet
New results about paths, segments, etc. The notion of simply_connected.
2016-03-14, by paulson
Merge
2016-03-14, by paulson
Refactoring (moving theorems into better locations), plus a bit of new material
2016-03-14, by paulson
strengthened tactics
2016-03-14, by blanchet
tuned;
2016-03-13, by wenzelm
tuned signature;
2016-03-13, by wenzelm
prefer Scala over bash function;
2016-03-13, by wenzelm
tuned;
2016-03-13, by wenzelm
clarified env;
2016-03-13, by wenzelm
unused;
2016-03-13, by wenzelm
more uniform signature for various process invocations;
2016-03-13, by wenzelm
tuned;
2016-03-13, by wenzelm
more theorems on orderings
2016-03-13, by haftmann
dropped junk
2016-03-13, by haftmann
tuned;
2016-03-12, by wenzelm
merged
2016-03-12, by wenzelm
tuned;
2016-03-12, by wenzelm
clarified cleanup;
2016-03-12, by wenzelm
more thorough cleanup -- in Scala;
2016-03-12, by wenzelm
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
2016-03-12, by wenzelm
obsolete (cf. 63a5782c764e);
2016-03-12, by wenzelm
clarified session build options: already provided by ML_Process;
2016-03-12, by wenzelm
spelling
2016-03-12, by haftmann
model characters directly as range 0..255
2016-03-12, by haftmann
tuned messages;
2016-03-11, by wenzelm
tuned message;
2016-03-11, by wenzelm
generate theorems like 'bool.split_sel'
2016-03-11, by blanchet
merged
2016-03-10, by wenzelm
tuned;
2016-03-10, by wenzelm
tuned;
2016-03-10, by wenzelm
upgrade "isabelle build" to Isabelle/Scala;
2016-03-10, by wenzelm
prefer plain "isabelle" from PATH within Isabelle settings environment;
2016-03-10, by wenzelm
isabelle_process is superseded by "isabelle process" tool;
2016-03-10, by wenzelm
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
2016-03-10, by wenzelm
clarified modules;
2016-03-10, by wenzelm
clarified files;
2016-03-10, by wenzelm
clarified files;
2016-03-10, by wenzelm
don't throw an exception when trying to print an error message
2016-03-10, by blanchet
eta-expansion done right in "primcorec"
2016-03-10, by blanchet
clarified: constructors in the sense of the code generator are not invertible;
2016-03-10, by haftmann
moved
2016-03-10, by haftmann
merged
2016-03-09, by wenzelm