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

discontinued ISABELLE_DOC_FORMAT;
2013-07-27, by wenzelm
more direct inclusion of tikz pictures;
2013-07-27, by wenzelm
obsolete;
2013-07-27, by wenzelm
documentation is always in PDF;
2013-07-27, by wenzelm
merged;
2013-07-27, by wenzelm
clarified Goal.stable_futures after 00170ef1dc39: running tasks are considered stable, without potentially blocking join;
2013-07-27, by wenzelm
clarified meaning of options for "isabelle options";
2013-07-27, by wenzelm
more correct context for dynamic invocations of static code conversions etc.
2013-07-27, by haftmann
support isabelle options -g;
2013-07-27, by wenzelm
tuned spelling;
2013-07-27, by wenzelm
tuned;
2013-07-27, by wenzelm
standardized aliases;
2013-07-27, by wenzelm
transfer rule for {c,d}tor_{,un}fold
2013-07-25, by traytel
two useful relation theorems
2013-07-25, by traytel
factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-07-25, by haftmann
derive specialized version of full fixpoint induction (with admissibility)
2013-07-24, by krauss
export mono_thm
2013-07-24, by krauss
merged Def_Init_Sound_X into Def_Init_X
2013-07-24, by nipkow
proper transfer rule format for map_transfer
2013-07-24, by traytel
merged
2013-07-24, by krauss
eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates
2013-07-23, by krauss
removed obsolete HOL-Boogie session;
2013-07-23, by boehmes
transfer stored bnf theorems into the "current" theory when retrieving a bnf (avoids non-trivial merges)
2013-07-23, by traytel
separate ML interface to note facts of a bnf
2013-07-23, by traytel
transfer rule for map (not yet registered as a transfer rule)
2013-07-22, by traytel
tuned exercises
2013-07-21, by nipkow
clarified option name, with improved sort order wrt. "time" options;
2013-07-20, by wenzelm
document update at high priority -- important;
2013-07-20, by wenzelm
option editor_execution_priority;
2013-07-20, by wenzelm
obscure options;
2013-07-20, by wenzelm
print_state at high priority -- fast and important;
2013-07-20, by wenzelm
proper Future.shutdown, to wait for the scheduler thread to finish remaining tasks (notably external processes);
2013-07-19, by wenzelm
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
2013-07-19, by wenzelm
just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
2013-07-19, by wenzelm
turned pattern unify flag into configuration option (global only);
2013-07-19, by wenzelm
merged
2013-07-19, by traytel
permissive uncheck -- allow printing of malformed terms (e.g. in error messages);
2013-07-19, by traytel
added exerciese
2013-07-19, by nipkow
do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)
2013-07-19, by traytel
modify background theory where it is actually required (cf. 51dfdcd88e84);
2013-07-18, by wenzelm
tuned messages -- avoid text folds stemming from Pretty.chunks;
2013-07-18, by wenzelm
proper system options for 'find_theorems';
2013-07-18, by wenzelm
guard unify tracing via visible status of global theory;
2013-07-18, by wenzelm
provide global operations as well;
2013-07-18, by wenzelm
tuned signature;
2013-07-18, by wenzelm
tuned;
2013-07-18, by wenzelm
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-18, by wenzelm
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
2013-07-18, by wenzelm
merged
2013-07-17, by wenzelm
tuned message;
2013-07-17, by wenzelm
tuned signature;
2013-07-17, by wenzelm
tuned
2013-07-17, by smolkas
merged
2013-07-17, by wenzelm
more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);
2013-07-17, by wenzelm
tuned spelling;
2013-07-17, by wenzelm
show variants in error messages; more precise error messages (give witnesses for multiple instances)
2013-07-17, by Christian Sternagel
refactoring
2013-07-17, by Christian Sternagel
more robust exn_messages_ids;
2013-07-17, by wenzelm
non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
2013-07-17, by wenzelm
take context from static theory, not dynamic theory certificate;
2013-07-17, by wenzelm

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

isabelle