Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
more explicit status for query operation;
2013-08-06, by wenzelm
tuned signature;
2013-08-06, by wenzelm
query process animation;
2013-08-05, by wenzelm
tuned signature;
2013-08-05, by wenzelm
tuning
2013-08-06, by blanchet
tuning
2013-08-06, by blanchet
tuning
2013-08-06, by blanchet
tuning
2013-08-06, by blanchet
export ML function (for primcorec)
2013-08-06, by blanchet
more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;
2013-08-05, by wenzelm
tuned proofs;
2013-08-05, by wenzelm
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
2013-08-05, by wenzelm
remove overlay after result has arrived -- one-shot query operation;
2013-08-05, by wenzelm
more message markup, provided by prover;
2013-08-05, by wenzelm
tuned signature -- more uniform treatment of overlays as command mapping;
2013-08-05, by wenzelm
commands with overlay remain visible, to avoid loosing printed output;
2013-08-05, by wenzelm
initial update of nodes_required, for proper GUI state;
2013-08-05, by wenzelm
tuned signature;
2013-08-05, by wenzelm
avoid repeated PIDE.flush_buffers when manipulating overlays;
2013-08-05, by wenzelm
tuned proofs;
2013-08-02, by wenzelm
merged
2013-08-02, by wenzelm
some actual find_theorems functionality;
2013-08-02, by wenzelm
more general Output.result: allow to update arbitrary properties;
2013-08-02, by wenzelm
prefer canonical order, to avoid potential fluctuation due to front-end edits;
2013-08-02, by wenzelm
tuned signature;
2013-08-02, by wenzelm
minimal print function "find_theorems", which merely echos its arguments;
2013-08-02, by wenzelm
support print functions with explicit arguments, as provided by overlays;
2013-08-02, by wenzelm
maintain overlays within node perspective;
2013-08-02, by wenzelm
some tracking of command location;
2013-08-02, by wenzelm
tuned proofs;
2013-08-02, by wenzelm
dockable window for "find" dialog (GUI only);
2013-08-02, by wenzelm
tuned;
2013-08-02, by wenzelm
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
2013-08-02, by traytel
more (co)datatype docs
2013-08-02, by blanchet
tuned exercises
2013-08-02, by nipkow
more (co)datatype documentation
2013-08-02, by blanchet
more (co)datatype documentation
2013-08-02, by blanchet
store relator induction in fp_result
2013-08-02, by traytel
merged
2013-08-01, by wenzelm
optional static analysis for Poly/ML 5.5.x;
2013-08-01, by wenzelm
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
2013-08-01, by wenzelm
recode utf8 for ML, as done in feeder.pl;
2013-08-01, by wenzelm
more explicit read-only non-TTY mode;
2013-08-01, by wenzelm
clarified options;
2013-08-01, by wenzelm
specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
2013-08-01, by wenzelm
tuned;
2013-08-01, by wenzelm
test recent polyml-svn, which is becoming polyml-5.5.1;
2013-08-01, by wenzelm
minor doc fixes
2013-08-01, by blanchet
more (co)datatype docs
2013-08-01, by blanchet
more (co)datatype documentation
2013-08-01, by blanchet
merged
2013-08-01, by kleing
removed duplicate lemma
2013-08-01, by kleing
more (co)datatype documentation
2013-08-01, by blanchet
tuning
2013-08-01, by blanchet
more (co)datatype docs
2013-08-01, by blanchet
tuned proof;
2013-08-01, by wenzelm
recovered "\<phi>\<^isub>i" from 0b02aaf7c7c5;
2013-07-31, by wenzelm
proper border (again) -- avoid NPE on Windows;
2013-07-31, by wenzelm
NEWS;
2013-07-31, by wenzelm
added home-made tooltips;
2013-07-31, by wenzelm
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
2013-07-31, by wenzelm
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
2013-07-31, by wenzelm
added Getting Started text
2013-07-31, by nipkow
more robust tactic
2013-07-31, by traytel
merged
2013-07-31, by wenzelm
clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
2013-07-31, by wenzelm
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
2013-07-31, by wenzelm
paint unassigned/unchanged nodes as unprocessed -- relevant for editor_continuous_checking = false;
2013-07-31, by wenzelm
allow explicit indication of required node: full eval, no prints;
2013-07-31, by wenzelm
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
2013-07-31, by wenzelm
more work on (co)datatype docs
2013-07-31, by blanchet
more (co)datatype documentation
2013-07-31, by blanchet
merged
2013-07-30, by wenzelm
tuned proofs;
2013-07-30, by wenzelm
more uniform border;
2013-07-30, by wenzelm
proper PIDE markup for codegen arguments;
2013-07-30, by wenzelm
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
2013-07-30, by wenzelm
tuned -- more uniform ML vs. Scala;
2013-07-30, by wenzelm
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
2013-07-30, by wenzelm
more timing;
2013-07-30, by wenzelm
more timing;
2013-07-30, by wenzelm
removed spurious headings
2013-07-30, by blanchet
more (co)datatype documentation
2013-07-30, by blanchet
avoid DUP error in local context
2013-07-30, by blanchet
sketched documentation for new (co)datatype package
2013-07-30, by blanchet
tuned docs (the function package isn't so new anymore)
2013-07-30, by blanchet
tuned comments;
2013-07-30, by wenzelm
tuned;
2013-07-30, by wenzelm
type theory is purely value-oriented;
2013-07-30, by wenzelm
pro-forma Execution.reset, despite lack of final join/commit;
2013-07-30, by wenzelm
tuned signature;
2013-07-30, by wenzelm
tuned;
2013-07-30, by wenzelm
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
2013-07-30, by wenzelm
merged
2013-07-29, by nipkow
tuned intro
2013-07-29, by nipkow
silenced subsumption warnings for default code equations entirely
2013-07-28, by haftmann
merged
2013-07-29, by wenzelm
NEWS;
2013-07-29, by wenzelm
tuned proofs;
2013-07-29, by wenzelm
updated key bindings to execution range;
2013-07-29, by wenzelm
traverse node on change of "required" state;
2013-07-29, by wenzelm
keep memo_exec execution running, which is important to cancel goal forks eventually;
2013-07-29, by wenzelm
maintain explicit execution frontier: avoid conflict with former task via static dependency;
2013-07-29, by wenzelm
afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;
2013-07-29, by wenzelm
clarified conditions for node traversal;
2013-07-29, by wenzelm
tuned;
2013-07-29, by wenzelm
pro-forma Goal.reset_futures, despite lack of final join/commit;
2013-07-29, by wenzelm
tuned;
2013-07-29, by wenzelm
tuned;
2013-07-29, by wenzelm
back to model.update_perspective with delay (cf. a20631db9c8a);
2013-07-29, by wenzelm
show displaced messages (e.g. from protocol thread) as raw output;
2013-07-29, by wenzelm
actually purge removed goal futures -- avoid memory leak;
2013-07-29, by wenzelm
tuned -- less redundant data structure;
2013-07-29, by wenzelm
always init GUI state;
2013-07-29, by wenzelm
tuned signature;
2013-07-29, by wenzelm
discontinued notion of "stable" result -- running execution is never canceled;
2013-07-29, by wenzelm
obsolete;
2013-07-29, by wenzelm
support declarative editor_execution_range, instead of old-style check/cancel buttons;
2013-07-29, by wenzelm
avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference
2013-07-29, by blanchet
updated Sledgehammer prover versions
2013-07-29, by blanchet
parse nonnumeric identifiers in E proofs correctly
2013-07-29, by blanchet
simplified Vampire hack -- no need to run it for other ATPs
2013-07-29, by blanchet
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
2013-07-29, by blanchet
prefer examples that work out of the box;
2013-07-28, by wenzelm
breakable @{file};
2013-07-28, by wenzelm
prefer existing swipl;
2013-07-28, by wenzelm
avoid machine running batch process for months;
2013-07-28, by wenzelm
more converse(p) theorems; tuned proofs;
2013-07-28, by traytel
more uniform cleanup;
2013-07-27, by wenzelm
tuned;
2013-07-27, by wenzelm
discontinued historic document formats;
2013-07-27, by wenzelm
avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;
2013-07-27, by wenzelm
tuned;
2013-07-27, by wenzelm
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
more official Thm.eq_thm_strict, without demanding ML equality type;
2013-07-17, by wenzelm
tuned;
2013-07-17, by wenzelm
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
2013-07-17, by immler
merged
2013-07-16, by wenzelm
Cygwin with Latex according to Cygwin-Latex-Setup.bat (presently unused);
2013-07-16, by wenzelm
overwrite target;
2013-07-16, by wenzelm
fully-automated packaging (requires Mac OS X);
2013-07-16, by wenzelm
more robust application init;
2013-07-16, by wenzelm
more self-contained application, with side-entry for init;
2013-07-16, by wenzelm
dispose intermediate 7z archive;
2013-07-16, by wenzelm
prefer stand-alone javaw;
2013-07-16, by wenzelm
more robust executable path specifications;
2013-07-16, by wenzelm
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
2013-07-16, by wenzelm
build Windows application on the spot, using Unix tools;
2013-07-16, by wenzelm
recover Cygwin symlinks via Windows file-system operations;
2013-07-15, by wenzelm
produce 7z archive for windows and preserve symlinks separately;
2013-07-15, by wenzelm
Scala version of init.bat;
2013-07-15, by wenzelm
tuned line length;
2013-07-15, by wenzelm
prefer @{file} references that are actually checked;
2013-07-15, by wenzelm
deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
2013-07-15, by wenzelm
retain compile-time context visibility, which is particularly important for "apply tactic";
2013-07-15, by wenzelm
use transfer/lifting for proving countable set and multisets being BNFs
2013-07-16, by traytel
added exercise
2013-07-16, by nipkow
killed unused theorems
2013-07-15, by traytel
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
2013-07-15, by traytel
tuned specifications and proofs;
2013-07-15, by wenzelm
tuned;
2013-07-15, by wenzelm
keep persistent prints only if actually finished;
2013-07-15, by wenzelm
more careful termination of removed execs, leaving running execs undisturbed;
2013-07-15, by wenzelm
recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
2013-07-14, by wenzelm
merged
2013-07-13, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
tip