isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 tip

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