isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

clarified;
2016-06-11, by wenzelm
clarified syntax;
2016-06-11, by wenzelm
spelling;
2016-06-11, by wenzelm
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
2016-06-10, by wenzelm
added command 'unbundle';
2016-06-10, by wenzelm
Merge
2016-06-10, by paulson
code to catch exception TERM in blast
2016-06-10, by paulson
merged
2016-06-10, by wenzelm
avoid duplicate Attrib.local_notes in aux. context;
2016-06-10, by wenzelm
proper restore;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
prefer hybrid 'bundle' command;
2016-06-10, by wenzelm
documentation;
2016-06-09, by wenzelm
clarified;
2016-06-09, by wenzelm
support for bundle definition via target;
2016-06-09, by wenzelm
tuned signature;
2016-06-09, by wenzelm
tuned;
2016-06-09, by wenzelm
tuned signature;
2016-06-09, by wenzelm
tuned;
2016-06-09, by wenzelm
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
2016-06-10, by paulson
merged
2016-06-09, by immler
approximation, derivative, and continuity of floor and ceiling
2016-06-09, by immler
remove smt call in Lebesge_Measure
2016-06-09, by hoelzl
proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
2016-06-08, by wenzelm
merged
2016-06-08, by wenzelm
NEWS;
2016-06-08, by wenzelm
tuned proofs;
2016-06-08, by wenzelm
provide dynamic facts in static context, to allow use of method_facts during static closure;
2016-06-08, by wenzelm
tuned;
2016-06-08, by wenzelm
clarified signature;
2016-06-07, by wenzelm
less ambitious arguments: thms only, no context declaration;
2016-06-07, by wenzelm
added method operator "use";
2016-06-07, by wenzelm
clarified signature;
2016-06-07, by wenzelm
clean facts more uniformly;
2016-06-07, by wenzelm
expode method_facts via dynamic method context;
2016-06-07, by wenzelm
tuned;
2016-06-07, by wenzelm
generalized bitlen to floor of log
2016-06-08, by immler
repair Unicode mess-up in c493859d4267
2016-06-08, by Andreas Lochbihler
NEWS and CONTRIBUTORS for SPMF
2016-06-08, by Andreas Lochbihler
merged
2016-06-08, by Andreas Lochbihler
import wasysym needed by Rewrite.thy
2016-06-07, by Andreas Lochbihler
add theory of discrete subprobability distributions
2016-06-07, by Andreas Lochbihler
clear distinction between different situations concerning strictness of code equations
2016-06-06, by haftmann
tuned signature
2016-06-06, by haftmann
more correct exception handling
2016-06-06, by haftmann
explicit tagging of code equations de-baroquifies interface
2016-06-06, by haftmann
dropped unused code
2016-06-06, by haftmann
conventional syntax for unit abstractions
2016-06-06, by haftmann
added action "isabelle.select-entity";
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
less redundant exploration of full name space;
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
avoid multiple reports on shared type;
2016-06-06, by wenzelm
updated to recent changes of Poly/ML directory layout;
2016-06-04, by wenzelm
tuned;
2016-06-04, by wenzelm
Integer.lcm normalizes the sign as in HOL/GCD.thy;
2016-06-04, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

isabelle