isabelle: Graph

thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world
2013-08-23, by blanchet
removed obsolete file
2013-08-23, by blanchet
minor MaSh fix
2013-08-23, by blanchet
eliminated some needless MaSh features
2013-08-23, by blanchet
tuned output
2013-08-23, by blanchet
better tracing + honor blocking better
2013-08-23, by blanchet
learn new facts on query if there aren't too many of them in MaSh
2013-08-23, by blanchet
remove OP
2013-08-23, by kuncar
increase relevance of unknown proximate facts
2013-08-22, by blanchet
fixed pattern matching
2013-08-22, by blanchet
fixed subtle bug with "take" + thread overlord through
2013-08-22, by blanchet
separate tracing option for code_simp
2013-08-22, by haftmann
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
2013-08-22, by haftmann
delete corresponding compound lhs and rhs when a transfer rule is deleted; tuned
2013-08-22, by kuncar
publish a private function
2013-08-22, by kuncar
configuration option to control timing output for (co)datatypes
2013-08-22, by traytel
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
2013-08-22, by blanchet
take chained and proximate facts into consideration when computing MaSh features
2013-08-22, by blanchet
pour extra features from proximate facts into goal, in exporter
2013-08-22, by blanchet
cleanup old duplicated functionality
2013-08-22, by blanchet
store theorem about composition of fold and map in fp_result
2013-08-22, by traytel
tuning
2013-08-22, by blanchet
ideas for (co)datatype docs
2013-08-22, by blanchet
minor tweaks to MaSh tool
2013-08-22, by blanchet
added datatype example
2013-08-22, by blanchet
support more brackets;
2013-08-21, by wenzelm
prefer text version of single angle quotation marks: U+2039 and U+203A from DejaVuSansMono;
2013-08-21, by wenzelm
double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
2013-08-21, by kuncar
improve weight computation for complex terms
2013-08-21, by blanchet
improved support for MaSh server
2013-08-21, by blanchet
get rid of some silly MaSh features
2013-08-21, by blanchet
weight MaSh constants by frequency
2013-08-21, by blanchet
transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids non-trivial merges)
2013-08-21, by traytel
reference to datatype refinment paper
2013-08-21, by haftmann
tuned theory imports
2013-08-21, by traytel
avoid constructor name clash
2013-08-21, by blanchet
renamed theory files to be closer to (new) command names
2013-08-21, by blanchet
only generate feature weights for queries -- they're not used elsewhere
2013-08-21, by blanchet
generate max suggestions in MaSh export driver
2013-08-21, by blanchet
new version of MaSh tool, with more server bugfixes
2013-08-21, by blanchet
take out dangerous feature, now that all updates are permanent
2013-08-21, by blanchet
use new MaSh command-line arguments
2013-08-21, by blanchet
shutdown MaSh server
2013-08-21, by blanchet
new version of MaSh tool, with less broken server
2013-08-21, by blanchet
merged
2013-08-20, by wenzelm
more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;
2013-08-20, by wenzelm
proper exhaustive match (cf. e9beabf045ab);
2013-08-20, by wenzelm
proper context;
2013-08-20, by wenzelm
merged
2013-08-20, by krauss
renamed theory Mrec to Legacy_Mrec, no longer included by default
2013-08-20, by krauss
replaced use of obsolete MREC by partial_function (heap)
2013-08-20, by krauss
more document antiquotations (for proper theorem names);
2013-08-17, by Christian Sternagel
moved derivation of strong coinduction to sugar
2013-08-20, by traytel
simpler (forward) derivation of strong (up-to equality) coinduction properties
2013-08-20, by traytel
don't derive unused low-level theorem
2013-08-20, by traytel
tuned example
2013-08-20, by traytel
doc tuning
2013-08-20, by blanchet
adapted ML code to new version of MaSh tool
2013-08-20, by blanchet
new version of MaSh tool -- experimental server
2013-08-20, by blanchet
adapted to new MaSh syntax
2013-08-20, by blanchet
tuning
2013-08-20, by blanchet
merged
2013-08-20, by paulson
Inserted footnote under match_tac
2013-08-20, by paulson
learn MaSh facts on the fly
2013-08-20, by blanchet
allow MaSh query to do some learning as well
2013-08-20, by blanchet
tuning
2013-08-20, by blanchet
merged
2013-08-20, by blanchet
removed french option to manuals
2013-08-20, by blanchet
treat frees as both consts and vars, for more hits
2013-08-19, by blanchet
keep long names to stay on the safe side
2013-08-19, by blanchet
tuned;
2013-08-19, by wenzelm
tuned signature;
2013-08-19, by wenzelm
MaSh tweaking: shorter names + killed (broken) SNoW
2013-08-19, by blanchet
handle Bounds as well in MaSh features
2013-08-19, by blanchet
add subtypes as well as features in MaSh
2013-08-19, by blanchet
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
2013-08-19, by blanchet
generate deep type patterns in MaSh
2013-08-19, by blanchet
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
2013-08-19, by blanchet
tuned;
2013-08-18, by wenzelm
tuned proofs;
2013-08-18, by wenzelm
more static simpsets, which also avoids spurious warnings due to duplicate rules provided here;
2013-08-18, by wenzelm
more symbols;
2013-08-18, by wenzelm
more symbols;
2013-08-18, by wenzelm
merged
2013-08-18, by wenzelm
load_theories if continuous_checking;
2013-08-18, by wenzelm
discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;
2013-08-18, by wenzelm
prefer plain subscript;
2013-08-18, by wenzelm
tuned;
2013-08-18, by wenzelm
spelling and typos
2013-08-18, by haftmann
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
2013-08-18, by haftmann
relaxed preconditions
2013-08-18, by haftmann
type class for generic division algorithm on numerals
2013-08-18, by haftmann
added lemma
2013-08-18, by haftmann
added lemma
2013-08-18, by haftmann
generalized sort constraint of lemmas
2013-08-18, by haftmann
explicit conversion from and to bool, and into algebraic structures with 0 and 1
2013-08-18, by haftmann
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
2013-08-18, by haftmann
more markup;
2013-08-18, by wenzelm
tuned;
2013-08-18, by wenzelm
updated identifier syntax;
2013-08-18, by wenzelm
Sledgehammer is docked on startup;
2013-08-17, by wenzelm
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
2013-08-17, by wenzelm
more robust startup;
2013-08-17, by wenzelm
some protocol to determine provers according to ML;
2013-08-17, by wenzelm
public access for protocol handlers and protocol commands -- to be used within reason;
2013-08-17, by wenzelm
always enable "minimize" to simplify interaction model;
2013-08-17, by wenzelm
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
2013-08-17, by wenzelm
recovered Locale.intern from d51bac27d4a0 (still used in AFP/Simp);
2013-08-17, by wenzelm
NEWS;
2013-08-17, by wenzelm
eliminated pointless subgoal argument;
2013-08-17, by wenzelm
more direct sledgehammer configuration via mode = Normal_Result and output_result;
2013-08-17, by wenzelm
more explicit sendback propertries based on mode;
2013-08-17, by wenzelm
tuned;
2013-08-16, by wenzelm
check_tool wrt. official ISABELLE_TOOLS;
2013-08-16, by wenzelm
more markup via Name_Space.check;
2013-08-16, by wenzelm
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
2013-08-16, by wenzelm
standardized aliases;
2013-08-16, by wenzelm
more markup -- avoid old Locale.extern;
2013-08-16, by wenzelm
renamed function
2013-08-16, by blanchet
eliminate quasi-duplicate function
2013-08-16, by blanchet
generalized "mk_permute"
2013-08-16, by blanchet
tuning
2013-08-16, by blanchet
added more functions to BNF library
2013-08-16, by blanchet
moved function to where it seems to belong
2013-08-16, by blanchet
moved library function where it belongs, and used Dmitriy's inside-out implementation
2013-08-16, by blanchet
added useful library function
2013-08-16, by blanchet
tuned
2013-08-16, by traytel
moved useful library functions upstream
2013-08-16, by blanchet
merge
2013-08-16, by blanchet
added fixme
2013-08-14, by blanchet
more (co)datatype documentation
2013-08-14, by blanchet
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
2013-08-14, by Andreas Lochbihler
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
2013-08-13, by traytel
more work on (co)datatype docs
2013-08-14, by blanchet
more symbolic notation;
2013-08-13, by wenzelm
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
2013-08-13, by wenzelm
merged
2013-08-13, by wenzelm
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
2013-08-13, by wenzelm
merged
2013-08-13, by wenzelm
more general window_geometry;
2013-08-13, by wenzelm
added rail diagram
2013-08-13, by blanchet
merged
2013-08-13, by wenzelm
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
2013-08-13, by wenzelm
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-08-13, by wenzelm
imported patch added_e_1_8
2013-08-13, by blanchet
remove unnecessary dependencies on Library/Quotient_*
2013-08-13, by kuncar
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
2013-08-13, by kuncar
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
2013-08-13, by kuncar
move useful lemmas to Main
2013-08-13, by kuncar
merged
2013-08-13, by wenzelm
indicate error-functions more prominently (by name prefix instead of suffix);
2013-08-09, by Christian Sternagel
avoid low-level Same structure;
2013-08-09, by Christian Sternagel
avoid misleading "instances" in function name;
2013-08-09, by Christian Sternagel
move treatment of polymorphism to adhoc overloading command;
2013-08-09, by Christian Sternagel
clarify function;
2013-08-09, by Christian Sternagel
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
2013-08-13, by wenzelm
imitate "noWordSep" of isabelle mode, e.g. relevant for word selection via double-click;
2013-08-13, by wenzelm
support somewhat standard "select all" by default;
2013-08-13, by wenzelm
more cleanup;
2013-08-13, by wenzelm
more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
2013-08-13, by wenzelm
tuned proofs;
2013-08-13, by wenzelm
added flag for jEdit/PIDE asynchronous mode
2013-08-13, by blanchet
updated Vampire version numbers
2013-08-13, by blanchet
Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
2013-08-13, by blanchet
whitepsace tuning
2013-08-13, by blanchet
more robust parsing of Vampire proofs with "introduced" names
2013-08-13, by blanchet
fixed "sorry"d proofs
2013-08-12, by blanchet
repaired proofs (after change to xxx_case_def)
2013-08-12, by blanchet
temporary sorry's for temporarily nonterminating (due to 2b430bbb5a1a) proofs
2013-08-12, by traytel
qualify intermediate typedefs
2013-08-12, by blanchet
avoid double qualification for case constants
2013-08-12, by blanchet
qualify more generated names with optional type name component
2013-08-12, by blanchet
eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)
2013-08-12, by traytel
generalized library function
2013-08-12, by traytel
updated keywords;
2013-08-12, by wenzelm
merged
2013-08-12, by wenzelm
clarified Query_Operation.register: avoid hard-wired parallel policy;
2013-08-12, by wenzelm
moved generic module to its proper place;
2013-08-12, by wenzelm
manage hyperlinks via PIDE editor interface;
2013-08-12, by wenzelm
tuned whitespace;
2013-08-12, by wenzelm
prefer PIDE editor operations;
2013-08-12, by wenzelm
central management of Document.Overlays, independent of Document_Model;
2013-08-12, by wenzelm
tuned -- use Multi_Map;
2013-08-12, by wenzelm
support for maps with multiple entries per key;
2013-08-12, by wenzelm
tuned signature;
2013-08-12, by wenzelm
tuned signature;
2013-08-12, by wenzelm
tuned signature;
2013-08-12, by wenzelm
tuned signature -- more abstract PIDE editor operations;
2013-08-12, by wenzelm
tuned messages
2013-08-12, by blanchet
clarified option name (since case/fold/rec are also destructors)
2013-08-12, by blanchet
define case constant from other 'free constructor' axioms
2013-08-12, by blanchet
introduced case tactics
2013-08-12, by blanchet
tuning
2013-08-12, by blanchet
handle both TVars and TFrees -- necessary for 'wrap_free_constructors'
2013-08-12, by blanchet
qualify map and rel names
2013-08-12, by blanchet
reverted ill-advised naming scheme of 5a77edcdbe54
2013-08-12, by blanchet
made (hopefully temporary) hack more robust
2013-08-11, by blanchet
added warning
2013-08-11, by blanchet
gracefully handle one more error condition
2013-08-11, by blanchet
gracefully fail to define polymorphic (co)datatypes in local context
2013-08-11, by blanchet
made code more robust
2013-08-11, by blanchet
avoid DUP exception in local context (cf. 062aa11e98e1)
2013-08-11, by blanchet
honor user tfree names
2013-08-11, by blanchet
prefer local facts over global ones
2013-08-10, by kleing
use local context for name space
2013-08-10, by kleing
explicit "strict" flag for print functions (flipped internal meaning);
2013-08-10, by wenzelm
avoid unnecessary case distinction
2013-08-10, by kleing
adjust tooltip for duplicates option
2013-08-10, by kleing
merged
2013-08-09, by wenzelm
NEWS;
2013-08-09, by wenzelm
Find is docked on startup;
2013-08-09, by wenzelm
sorted lines;
2013-08-09, by wenzelm
tuned GUI;
2013-08-09, by wenzelm
retain current task priority, to avoid distortion due to local forks (e.g. sledgehammer query operation);
2013-08-09, by wenzelm
removed "Locate" button, to avoid confusion about the slightly odd meaning of current_command with explicit theory context;
2013-08-09, by wenzelm
enable search in pre-loaded theory;
2013-08-09, by wenzelm
more GUI options;
2013-08-09, by wenzelm
tuned signature;
2013-08-09, by wenzelm
tuned;
2013-08-09, by wenzelm
tuned GUI;
2013-08-09, by wenzelm
tuned name generation code (to make it easier to adapt later)
2013-08-09, by blanchet
honor user type names if possible
2013-08-09, by blanchet
merged;
2013-08-09, by wenzelm
more abstract consume_status operation;
2013-08-09, by wenzelm
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
2013-08-09, by wenzelm
more active "provers" field, which increases chances that its history is stored;
2013-08-09, by wenzelm
removed command location is considered finished, and its overlay removed eventually;
2013-08-09, by wenzelm
cancel_query via direct access to the exec_id of the running query process;
2013-08-09, by wenzelm
retain original messages properties, e.g. for retrieval via Command.Results;
2013-08-09, by wenzelm
clarified toplevel_error: absorb and print interrupts;
2013-08-09, by wenzelm
more explicit error;
2013-08-09, by wenzelm
tuned message;
2013-08-09, by wenzelm
removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
2013-08-08, by wenzelm
more robust read_query;
2013-08-08, by wenzelm
removed commented out declaration
2013-08-09, by kleing
tuned
2013-08-09, by traytel
merged
2013-08-08, by wenzelm
eliminate \<twosuperior> as well;
2013-08-08, by wenzelm
more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
2013-08-08, by wenzelm
prefer plain subscript for identifiers;
2013-08-08, by wenzelm
proper low-level comparison -- heed warning by Scala compiler;
2013-08-08, by wenzelm
merged
2013-08-08, by Andreas Lochbihler
prefer Code.abort with explicit error message
2013-08-08, by Andreas Lochbihler
avoid re-inventing transitive closure
2013-08-08, by kleing
merged
2013-08-08, by traytel
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
2013-08-08, by traytel
tuned
2013-08-08, by traytel
tuned tactic;
2013-08-08, by traytel
abort execution of generated code with explicit exception message
2013-08-08, by Andreas Lochbihler
merged
2013-08-08, by wenzelm
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
2013-08-08, by wenzelm
tuned imports;
2013-08-08, by wenzelm
snippet for instr type
2013-08-08, by kleing
filter function on streams
2013-08-08, by traytel
tuned
2013-08-08, by traytel
tuned proofs;
2013-08-07, by wenzelm
tuned proofs;
2013-08-07, by wenzelm
maintain commands together with index -- avoid redundant reconstruction of full_index;
2013-08-07, by wenzelm
more elementary list structures for markup tree traversal;
2013-08-07, by wenzelm
tuning
2013-08-07, by blanchet
enrich exported ML function's signature
2013-08-07, by blanchet
merged
2013-08-07, by wenzelm
more NEWS and CONTRIBUTORS;
2013-08-07, by wenzelm
some documentation for adhoc overloading;
2013-08-02, by Christian Sternagel
added examples of adhoc overloading
2013-08-02, by Christian Sternagel
use uniform spelling of "adhoc"
2013-08-02, by Christian Sternagel
tuned formatting of error message
2013-08-02, by Christian Sternagel
tuned proofs;
2013-08-07, by wenzelm
tuned signature;
2013-08-07, by wenzelm
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
2013-08-07, by wenzelm
tuned;
2013-08-07, by wenzelm
tuned signature;
2013-08-07, by wenzelm
enabled key event to apply query;
2013-08-07, by wenzelm
prefer single-line HistoryTextField;
2013-08-07, by wenzelm
contract equalities in transfer and transfer domain rules when they are registered
2013-08-07, by kuncar
expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
2013-08-07, by kuncar
merged
2013-08-06, by wenzelm
misc tuning and simplification;
2013-08-06, by wenzelm
more generic button;
2013-08-06, by wenzelm
support for query operations that consist of parallel segments;
2013-08-06, by wenzelm
more tooltips;
2013-08-06, by wenzelm
tuned -- more explicit type Status.Value;
2013-08-06, by wenzelm
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