Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+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.
prefer explicit link;
2017-06-30, by wenzelm
updated package;
2017-06-29, by wenzelm
provide --baseImagesUrl for VSCode extensions marketplace;
2017-06-29, by wenzelm
tuned;
2017-06-29, by wenzelm
updated package;
2017-06-29, by wenzelm
tuned;
2017-06-29, by wenzelm
added screenshot;
2017-06-29, by wenzelm
clarified;
2017-06-29, by wenzelm
updated package;
2017-06-29, by wenzelm
tuned;
2017-06-29, by wenzelm
tuned output;
2017-06-29, by wenzelm
tuned spelling;
2017-06-29, by wenzelm
more documentation;
2017-06-29, by wenzelm
auto update;
2017-06-29, by wenzelm
clarified editor focus;
2017-06-29, by wenzelm
proper hyperlink_command, notably for locate_query;
2017-06-29, by wenzelm
tuned signature;
2017-06-29, by wenzelm
proper dynamic controls, notably for auto_update_enabled;
2017-06-29, by wenzelm
tuned signature;
2017-06-29, by wenzelm
HTML GUI actions via JavaScript;
2017-06-29, by wenzelm
more operations/options;
2017-06-28, by wenzelm
clarified signature;
2017-06-28, by wenzelm
merged
2017-06-27, by wenzelm
support for HTTP/POST method;
2017-06-27, by wenzelm
clarified defaults;
2017-06-27, by wenzelm
tuned signature;
2017-06-27, by wenzelm
auto update;
2017-06-27, by wenzelm
added missing files (cf. 5aa9cb83e70e);
2017-06-27, by wenzelm
auto update;
2017-06-27, by wenzelm
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
2017-06-27, by wenzelm
GUI layout similar to Pure/GUI/wrap_panel.scala;
2017-06-27, by wenzelm
Removed more "guess", etc.
2017-06-27, by paulson
more error checking
2017-06-27, by blanchet
merged
2017-06-26, by wenzelm
some HTML GUI elements;
2017-06-26, by wenzelm
proper bootstrap_name (amending b42743f5b595);
2017-06-26, by wenzelm
clarified indentation;
2017-06-26, by wenzelm
More tidying of horrible proofs
2017-06-26, by paulson
A few renamings and several tidied-up proofs
2017-06-26, by paulson
back to scala-2.12.2, after a41435469559;
2017-06-24, by wenzelm
more direct construction of integer_of_num;
2017-06-24, by haftmann
treat "undefined" constants internally as special form of case combinators
2017-06-24, by haftmann
Improved error reporting when activating a locale instance (beyond syntax decls).
2017-06-24, by ballarin
Additional corollary Knaster_Tarski_idem_inf_eq.
2017-06-24, by ballarin
clarified indentation;
2017-06-24, by wenzelm
clarified indentation;
2017-06-24, by wenzelm
merged
2017-06-23, by wenzelm
tuned signature;
2017-06-23, by wenzelm
tuned;
2017-06-23, by wenzelm
NEWS;
2017-06-23, by wenzelm
indentation of keywords after input;
2017-06-23, by wenzelm
indent = 0 for blank lines: produce less whitespace by default;
2017-06-23, by wenzelm
clarified prev_line: stop at blank line;
2017-06-23, by wenzelm
more information;
2017-06-23, by wenzelm
tuned signature;
2017-06-23, by wenzelm
tuned;
2017-06-23, by wenzelm
avoid trailing spaces;
2017-06-23, by wenzelm
clarified modules;
2017-06-23, by wenzelm
Merged
2017-06-23, by eberlm
distrib_lattice instance for filters
2017-06-23, by eberlm
merged
2017-06-22, by wenzelm
keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
2017-06-22, by wenzelm
consolidate proofs more simultaneously;
2017-06-22, by wenzelm
more informative task_statistics;
2017-06-22, by wenzelm
more informative task_statistics;
2017-06-22, by wenzelm
Merge
2017-06-22, by paulson
New theorems and much tidying up of the old ones
2017-06-22, by paulson
added 'solvers' option to Nunchaku
2017-06-22, by blanchet
Contravariant map on filters
2017-06-22, by eberlm
merged
2017-06-21, by wenzelm
tuned granularity of parallel tasks;
2017-06-21, by wenzelm
more completion;
2017-06-21, by wenzelm
clarified modules;
2017-06-21, by wenzelm
tuned signature;
2017-06-21, by wenzelm
added -d option to Mirabelle
2017-06-21, by blanchet
stripped code pre/postprocessor setup for real from superfluous rules
2017-06-20, by haftmann
Tidying up integration theory and some new theorems
2017-06-21, by paulson
more completion;
2017-06-21, by wenzelm
tuned signature;
2017-06-21, by wenzelm
tuned signature;
2017-06-21, by wenzelm
tuned signature;
2017-06-21, by wenzelm
deleting a code equation never leads to unimplemented function
2017-06-20, by haftmann
avoid ancient [code, code del] antipattern
2017-06-20, by haftmann
obsolete
2017-06-20, by haftmann
register equations stemming from extracted proofs as specification rules
2017-06-20, by haftmann
tuned
2017-06-20, by haftmann
merged
2017-06-20, by wenzelm
tuned signature;
2017-06-20, by wenzelm
proper treatment of empty result;
2017-06-20, by wenzelm
clarified modules;
2017-06-20, by wenzelm
tuned signature;
2017-06-20, by wenzelm
provide spell-checker menu via completion commands;
2017-06-20, by wenzelm
added commands for spell-checker dictionary;
2017-06-20, by wenzelm
tuned signature;
2017-06-20, by wenzelm
tuning
2017-06-20, by blanchet
SMT news
2017-06-20, by blanchet
correctly unfold applied 'let's (e.g. '(let x = a in f) b') -- and removed dead code
2017-06-20, by blanchet
do not print unimplemented functions
2017-06-20, by haftmann
dropped void values
2017-06-20, by haftmann
more uniform order of constructors
2017-06-20, by haftmann
more consistent terminology
2017-06-20, by haftmann
avoid name particle "the" where no selection is implied
2017-06-20, by haftmann
more uniform ordering and naming of sections;
2017-06-20, by haftmann
tuned internal signature
2017-06-20, by haftmann
more explicit constructor name
2017-06-20, by haftmann
tuned whitespace
2017-06-20, by haftmann
replaced recdef by fun
2017-06-20, by haftmann
spelling
2017-06-20, by haftmann
merged
2017-06-19, by wenzelm
added spell-checker completion;
2017-06-19, by wenzelm
clarified modules;
2017-06-19, by wenzelm
tuned;
2017-06-19, by wenzelm
clarified modules;
2017-06-19, by wenzelm
tuned signature;
2017-06-19, by wenzelm
clarified modules;
2017-06-19, by wenzelm
tuned;
2017-06-19, by wenzelm
clarified signature;
2017-06-19, by wenzelm
Repaired an inadvertent reordering of the premises of two theorems
2017-06-19, by paulson
New theorems; stronger theorems; tidier theorems. Also some renaming
2017-06-19, by paulson
merged
2017-06-17, by nipkow
adapted to new simp lemmas
2017-06-17, by nipkow
added simp rules
2017-06-17, by nipkow
more permissive: avoid situations where query is silently ignored;
2017-06-17, by wenzelm
more robust: do not touch unrelated directory isabelle_repos_other (i.e. bad argument);
2017-06-17, by wenzelm
always start with fresh clone (with explicitly given rev): more robust on Windows;
2017-06-17, by wenzelm
reverted 94cad7590015: does not help much on Windows;
2017-06-17, by wenzelm
tuned signature;
2017-06-17, by wenzelm
merged
2017-06-17, by wenzelm
updated package;
2017-06-17, by wenzelm
maintain overlays within main state of document models;
2017-06-17, by wenzelm
proper treatment of editor overlays;
2017-06-16, by wenzelm
tuned;
2017-06-16, by wenzelm
clarified modules;
2017-06-16, by wenzelm
tuned signature;
2017-06-16, by wenzelm
support for separate proof state output;
2017-06-16, by wenzelm
automatic reformatting;
2017-06-16, by wenzelm
more general dispatcher operations;
2017-06-16, by wenzelm
tuned;
2017-06-14, by wenzelm
clarified modules;
2017-06-14, by wenzelm
tuned;
2017-06-14, by wenzelm
tuned;
2017-06-14, by wenzelm
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
2017-06-15, by paulson
tuned
2017-06-15, by nipkow
simplified delete/proof
2017-06-14, by nipkow
clarified signature;
2017-06-13, by wenzelm
added abstract editor operations, notably for Query_Operation;
2017-06-13, by wenzelm
tuned signature;
2017-06-13, by wenzelm
tuned;
2017-06-13, by wenzelm
clarified modules;
2017-06-13, by wenzelm
clarified modules;
2017-06-13, by wenzelm
updated package;
2017-06-13, by wenzelm
tuned GUI;
2017-06-13, by wenzelm
obsolete;
2017-06-13, by wenzelm
removed pointless entries: not part of api.LanguageEntry;
2017-06-12, by wenzelm
avoid overlapping line background, notably for "quoted";
2017-06-12, by wenzelm
tuned rendering;
2017-06-12, by wenzelm
tuned;
2017-06-12, by wenzelm
clarified message;
2017-06-12, by wenzelm
retain vacuous CompletionProvider for now;
2017-06-12, by wenzelm
tuned;
2017-06-12, by wenzelm
dynamic configuration of prettify-symbols-mode, similar to VSCoq;
2017-06-12, by wenzelm
obsolete;
2017-06-12, by wenzelm
removed pointless default: vscode.previewHtml happens only after prover response;
2017-06-12, by wenzelm
more markup for HTML rendering;
2017-06-12, by wenzelm
tuned signature;
2017-06-12, by wenzelm
clarified;
2017-06-12, by wenzelm
tuned;
2017-06-12, by wenzelm
superseded by external protocol;
2017-06-10, by wenzelm
use old-style "textEdit" for the sake of the external protocol (see also vscode-languageserver-node/issues/188);
2017-06-10, by wenzelm
tuned;
2017-06-10, by wenzelm
symbol completion that bypasses the LS protocol, and thus observes the range properly;
2017-06-10, by wenzelm
More rules for Probability/Tree_Space
2017-06-10, by eberlm
merged
2017-06-09, by wenzelm
tuned;
2017-06-09, by wenzelm
clarified output for symbol completion;
2017-06-09, by wenzelm
tuned;
2017-06-09, by wenzelm
more uniform syntax_completion + semantic_completion;
2017-06-09, by wenzelm
clarified modules;
2017-06-09, by wenzelm
provide information about Isabelle symbols within VSCode;
2017-06-09, by wenzelm
tuned signature;
2017-06-09, by wenzelm
Cleaned up and extended Probability/Tree_Space
2017-06-09, by eberlm
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
2017-06-09, by hoelzl
avoid markup, for the sake of Build_Log.Log_File.parse_props;
2017-06-09, by wenzelm
more robust: store important meta info before potential failure;
2017-06-09, by wenzelm
tuned message;
2017-06-09, by wenzelm
merged
2017-06-09, by wenzelm
more HTML rendering as in Isabelle/jEdit;
2017-06-08, by wenzelm
tuned signature;
2017-06-08, by wenzelm
clarified menu;
2017-06-08, by wenzelm
clarified signature;
2017-06-08, by wenzelm
HTML preview based on PIDE markup;
2017-06-08, by wenzelm
explicit foreground color, for the sake of dark theme in VSCode;
2017-06-08, by wenzelm
tuned layout (amending 8040d2563593);
2017-06-08, by wenzelm
more official session qualifier;
2017-06-08, by wenzelm
clarified;
2017-06-08, by wenzelm
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
2017-06-08, by boehmes
merged
2017-06-07, by wenzelm
clarified output;
2017-06-07, by wenzelm
more tooltips;
2017-06-07, by wenzelm
clarified imports;
2017-06-07, by wenzelm
update strictly local imports only;
2017-06-07, by wenzelm
proper imports_base;
2017-06-07, by wenzelm
tuned;
2017-06-07, by wenzelm
avoid redundant Preview documents;
2017-06-07, by wenzelm
HOL-Probability: add measurable space for trees
2017-06-07, by hoelzl
clarified import of loaded theory;
2017-06-06, by wenzelm
decomposed tuple
2017-06-05, by haftmann
tuned
2017-06-05, by haftmann
clarified message
2017-06-05, by haftmann
tuned signature;
2017-06-06, by wenzelm
discontinued obsolete print mode;
2017-06-06, by wenzelm
HTML preview via builtin HTTP server;
2017-06-05, by wenzelm
permissive output of XML.Text, e.g. relevant for embedded <style>;
2017-06-05, by wenzelm
avoid Local_Theory.reset in application space
2017-06-05, by haftmann
tuned
2017-06-05, by haftmann
specific output setup is not supposed to intrude regular import theory
2017-06-05, by haftmann
avoid duplicate
2017-06-05, by haftmann
streamlined code setup for fake terms
2017-06-05, by haftmann
modernized (code) setup for enumeration predicates
2017-06-05, by haftmann
simplified setup
2017-06-05, by haftmann
executable domain membership checks
2017-06-05, by haftmann
more tests;
2017-06-05, by wenzelm
cover more history;
2017-06-05, by wenzelm
cover more history;
2017-06-05, by wenzelm
uniform notion of Symbol.is_controllable (see also 265d9300d523);
2017-06-05, by wenzelm
merged
2017-06-02, by lammich
Added char, ref, array to heap-storable types
2017-06-01, by lammich
Fixed to also work with non-IntInf default int type
2017-06-01, by lammich
updated package;
2017-06-01, by wenzelm
proper markup for IsabelleText font;
2017-06-01, by wenzelm
generate CSS for Isabelle fonts;
2017-06-01, by wenzelm
tuned signature;
2017-06-01, by wenzelm
tuned signature;
2017-06-01, by wenzelm
output control symbols like ML version, with optionally hidden source;
2017-06-01, by wenzelm
use css from Isabelle distribution;
2017-06-01, by wenzelm
clarified output;
2017-06-01, by wenzelm
proper update of already existing preview;
2017-06-01, by wenzelm
tuned signature;
2017-06-01, by wenzelm
tuned signature;
2017-06-01, by wenzelm
tuned;
2017-06-01, by wenzelm
uniform output of HTML as XML;
2017-06-01, by wenzelm
tuned layout;
2017-05-31, by wenzelm
modernized generated HTML;
2017-05-31, by wenzelm
tuned signature;
2017-05-31, by wenzelm
added update operation;
2017-05-31, by wenzelm
clarified name;
2017-05-31, by wenzelm
register commands earlier, before prover startup;
2017-05-31, by wenzelm
explicit preview request/response;
2017-05-31, by wenzelm
tuned layout;
2017-05-31, by wenzelm
more robust -- avoid race condition wrt. Haskell output in $ISABELLE_TMP/examples/
2017-05-31, by wenzelm
merged
2017-05-30, by wenzelm
tuned -- like Dynamic_Preview;
2017-05-30, by wenzelm
tuned;
2017-05-30, by wenzelm
provide preview content on Scala side (similar to output);
2017-05-30, by wenzelm
tuned signature;
2017-05-30, by wenzelm
more careful treatment of context.subscriptions;
2017-05-30, by wenzelm
clarified event handling;
2017-05-30, by wenzelm
tuned;
2017-05-30, by wenzelm
clarified modules;
2017-05-30, by wenzelm
tuned;
2017-05-30, by wenzelm
clarified modules;
2017-05-30, by wenzelm
tuned imports;
2017-05-30, by wenzelm
clarified modules;
2017-05-30, by wenzelm
clarified signature;
2017-05-30, by wenzelm
clarified modules;
2017-05-30, by wenzelm
tuned names
2017-05-30, by nipkow
adjusted doc
2017-05-30, by nipkow
redefined Greatest
2017-05-30, by nipkow
merged
2017-05-29, by wenzelm
update preview after document change;
2017-05-29, by wenzelm
proper HTML preview;
2017-05-29, by wenzelm
clarified view column;
2017-05-29, by wenzelm
basic setup for document preview;
2017-05-29, by wenzelm
Tuned Library/Sublist.thy
2017-05-29, by eberlm
reorganised material on sublists
2017-05-29, by eberlm
removed GreatestM
2017-05-28, by nipkow
introduced arg_max
2017-05-28, by nipkow
added is_arg_min
2017-05-28, by nipkow
removed LeastM; is now arg_min
2017-05-28, by nipkow
more arg_min
2017-05-27, by nipkow
no exit code from build processes by default, e.g. relevant for non-strict results of remote_build_history;
2017-05-27, by wenzelm
tuned;
2017-05-27, by wenzelm
clarified build errors;
2017-05-27, by wenzelm
tuned layout;
2017-05-27, by wenzelm
tuned signature;
2017-05-27, by wenzelm
tuned signature;
2017-05-27, by wenzelm
tuned signature;
2017-05-27, by wenzelm
tuned signature;
2017-05-27, by wenzelm
clarified signature;
2017-05-27, by wenzelm
tuned layout;
2017-05-27, by wenzelm
show errors from build_log database;
2017-05-26, by wenzelm
support for message underline and tooltips;
2017-05-26, by wenzelm
unused;
2017-05-26, by wenzelm
store errors in build_history logs and database;
2017-05-26, by wenzelm
tuned;
2017-05-26, by wenzelm
more selective database access;
2017-05-26, by wenzelm
store errors in build db;
2017-05-26, by wenzelm
more correct and complete output of control characters;
2017-05-26, by wenzelm
clarified modules;
2017-05-26, by wenzelm
do not expose ML interrupt in Scala;
2017-05-26, by wenzelm
tuned signature;
2017-05-26, by wenzelm
prefer strict result (in contrast to 0f3b0a929c02);
2017-05-25, by wenzelm
avoid conflict with generated settings of other_isabelle;
2017-05-25, by wenzelm
more progress information, for the sake of sporadic dropouts;
2017-05-25, by wenzelm
restricted perspective depending on the caret -- important for reactivity when editing big files;
2017-05-25, by wenzelm
parallel retrieval of PIDE markup;
2017-05-25, by wenzelm
clarified output: do not require "method", which is absent for ResponseMessage;
2017-05-25, by wenzelm
tuned;
2017-05-25, by wenzelm
clarified message logging;
2017-05-25, by wenzelm
more operations;
2017-05-25, by wenzelm
clarified signature;
2017-05-25, by wenzelm
obsolete special case
2017-05-25, by haftmann
tuned message;
2017-05-24, by wenzelm
proper ISABELLE_IDENTIFIER for remote Admin/build_history, e.g. relevant for settings;
2017-05-24, by wenzelm
tuned;
2017-05-24, by wenzelm
proper index;
2017-05-24, by wenzelm
updated package;
2017-05-23, by wenzelm
support text overview colors via decorations;
2017-05-23, by wenzelm
tuned;
2017-05-23, by wenzelm
clarified modules;
2017-05-23, by wenzelm
clarified build.out progress;
2017-05-23, by wenzelm
more persistent build.out;
2017-05-23, by wenzelm
tuned;
2017-05-23, by wenzelm
less ambitious parallelism to make this work more robustly on Windows;
2017-05-22, by wenzelm
more settings;
2017-05-22, by wenzelm
support for ISABELLE_GHC on Windows, using the native version (mingw32);
2017-05-22, by wenzelm
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
2017-05-22, by wenzelm
clarified signature;
2017-05-22, by wenzelm
more settings;
2017-05-22, by wenzelm
more robust treatment of generated strings;
2017-05-22, by wenzelm
proper File.platform_path for scala on Windows;
2017-05-22, by wenzelm
removed junk;
2017-05-22, by wenzelm
proper File.platform_path for poly on Windows;
2017-05-22, by wenzelm
back to scala-2.11.8 due to apparent non-termination of HOL-Codegenerator_Test;
2017-05-22, by wenzelm
suppress failed sessions, since Jenkins entries lack ISABELLE_BUILD_OPTIONS with threads (see also 744878d72021);
2017-05-21, by wenzelm
more general workaround for failed sessions (again, see also 2edb89630a80, ed7b5cd3a7f2);
2017-05-21, by wenzelm
merged
2017-05-21, by wenzelm
show failed sessions on main page;
2017-05-21, by wenzelm
clarified signature;
2017-05-21, by wenzelm
HTML rendering based on Isabelle/jEdit colors;
2017-05-21, by wenzelm
refer to already extracted library files, to avoid tmp files produced by SQLiteJDBCLoader, which tend to remain after JVM crash;
2017-05-21, by wenzelm
incremental build progress, to see state after unexpected failure (see also b3d6fb291f58);
2017-05-21, by wenzelm
more Progress variations;
2017-05-21, by wenzelm
more systematic separation of build_history directories (see also 80c1c1f53e72);
2017-05-21, by wenzelm
updated dependencies;
2017-05-21, by wenzelm
added one more simplification to help replay
2017-05-21, by blanchet
adapt to Scala 2.12.x
2017-05-21, by Lars Hupel
updated to postgresql-42.1.1;
2017-05-20, by wenzelm
updated to sqlite-jdbc-3.18.0;
2017-05-20, by wenzelm
keep main build.log to help diagnosing spurious lack of log_path.xz;
2017-05-20, by wenzelm
clarified build_polyml_component;
2017-05-19, by wenzelm
avoid mixture of symlinks and hardlinks, which causes problems with BSD tar on macOS Sierra;
2017-05-19, by wenzelm
updated;
2017-05-19, by wenzelm
more uniform line-oriented output, notably for scala-2.12.2 REPL which emits "\n" separately;
2017-05-19, by wenzelm
tuned;
2017-05-19, by wenzelm
suppress ANSI control sequences in Scala console;
2017-05-19, by wenzelm
updated to scala-2.12.2;
2017-05-19, by wenzelm
updated to jdk-8u131;
2017-05-19, by wenzelm
updated to xz-java-1.6;
2017-05-19, by wenzelm
separate keep auxiliary directory, to facilitate error diagnosis;
2017-05-19, by wenzelm
Merged
2017-05-18, by eberlm
more on sublists
2017-05-18, by eberlm
tuned;
2017-05-18, by wenzelm
more charts;
2017-05-18, by wenzelm
uniform heap_scale;
2017-05-18, by wenzelm
more plots from ml_statistics;
2017-05-18, by wenzelm
simplified signature;
2017-05-18, by wenzelm
tuned signature;
2017-05-18, by wenzelm
more JFreeChart operations;
2017-05-18, by wenzelm
do not store bulky ml_statistics;
2017-05-17, by wenzelm
more output;
2017-05-17, by wenzelm
plot average heap size;
2017-05-17, by wenzelm
more systematic maximum and average;
2017-05-17, by wenzelm
clarified use of XML.Cache;
2017-05-17, by wenzelm
proper ml_statistics;
2017-05-17, by wenzelm
store processed content instead of somewhat bulky properties;
2017-05-17, by wenzelm
include full ML statistics: max heap size;
2017-05-17, by wenzelm
tuned;
2017-05-17, by wenzelm
eliminated unused operations;
2017-05-17, by wenzelm
tuned signature;
2017-05-17, by wenzelm
clarified universal table: include ml_statistics;
2017-05-17, by wenzelm
proper order for entry list cons;
2017-05-17, by wenzelm
proper check (amending ad35427dbe88);
2017-05-17, by wenzelm
less restrictive filter: omit empty charts, but show latest timing;
2017-05-16, by wenzelm
prefer explicit output file: potentially more robust than stdout;
2017-05-16, by wenzelm
proper init_settings, before inspecting ML_HOME etc;
2017-05-16, by wenzelm
support for explicit output file: potentially more robust than stdout;
2017-05-16, by wenzelm
proper init_settings for init_component (before generated ML_OPTIONS etc.);
2017-05-16, by wenzelm
more arg_min
2017-05-16, by nipkow
NEWS;
2017-05-15, by wenzelm
history parameters like "Linux A", for more comparable results;
2017-05-15, by wenzelm
merged
2017-05-14, by wenzelm
tuned signature;
2017-05-14, by wenzelm
style for <dl> that is reminiscent of LaTeX;
2017-05-14, by wenzelm
more systematic HTML.init_dir with css;
2017-05-14, by wenzelm
prefer logical markup;
2017-05-14, by wenzelm
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
2017-05-14, by wenzelm
tuned signature;
2017-05-14, by wenzelm
implicitly check for unknown files (not part of a Mercurial repository);
2017-05-14, by wenzelm
prefer explicit progress channel;
2017-05-14, by wenzelm
prefer explicit progress channel;
2017-05-14, by wenzelm
more explicit warning/error messages;
2017-05-14, by wenzelm
tuned signature;
2017-05-14, by wenzelm
tuned;
2017-05-14, by wenzelm
clarified interface;
2017-05-14, by wenzelm
more robust command invocation, without defaults from hgrc;
2017-05-14, by wenzelm
clarified: repository files before commit;
2017-05-14, by wenzelm
eliminated suspicious Unicode;
2017-05-14, by wenzelm
clarified notion of known files (before actual commit);
2017-05-14, by wenzelm
explore older history;
2017-05-14, by wenzelm
explicit history_base;
2017-05-14, by wenzelm
explore repository structure, with minimal assumptions about "hg log" output;
2017-05-14, by wenzelm
avoid hardlinks, for more robustness on Windows file-systems;
2017-05-14, by wenzelm
added function arg_min
2017-05-14, by nipkow
merged
2017-05-14, by nipkow
added lemma
2017-05-14, by nipkow
obsolete (see also bdd17b18e103, f533820e7248);
2017-05-14, by wenzelm
relaxed theory dependencies
2017-05-12, by haftmann
explicit theory for factorials
2017-05-12, by haftmann
more lemmas
2017-05-11, by haftmann
explore older history;
2017-05-12, by wenzelm
more explicit flag for historic builds;
2017-05-12, by wenzelm
proper result for rev == "";
2017-05-12, by wenzelm
tuned -- more open to experimentation;
2017-05-12, by wenzelm
tuned -- more visible;
2017-05-12, by wenzelm
updated to polyml-5.7 for testing (not yet ready for production use);
2017-05-12, by wenzelm
tuned;
2017-05-12, by wenzelm
notes on gnuplot;
2017-05-10, by wenzelm
tuned;
2017-05-10, by wenzelm
made SMT reconstruction more complete (bug report by Lukas Bulwahn)
2017-05-10, by blanchet
tuning
2017-05-10, by blanchet
stretch image according to history length;
2017-05-10, by wenzelm
actually plot extended profile history;
2017-05-10, by wenzelm
tuned output;
2017-05-10, by wenzelm
more output;
2017-05-09, by wenzelm
clarified;
2017-05-09, by wenzelm
tuned output;
2017-05-09, by wenzelm
more robust update of generated directory;
2017-05-09, by wenzelm
more output;
2017-05-09, by wenzelm
tuned;
2017-05-09, by wenzelm
obsolete;
2017-05-09, by wenzelm
enter deeper into history;
2017-05-09, by wenzelm
more Jenkins test results;
2017-05-09, by wenzelm
clarified order of output;
2017-05-09, by wenzelm
tuned;
2017-05-09, by wenzelm
tuned signature;
2017-05-09, by wenzelm
tuned message;
2017-05-08, by wenzelm
pick isabelle_version based on build_log database;
2017-05-08, by wenzelm
simplified default;
2017-05-08, by wenzelm
tuned (again);
2017-05-08, by wenzelm
allow column with defining expression;
2017-05-08, by wenzelm
tuned -- inlined single use;
2017-05-08, by wenzelm
tuned signature;
2017-05-08, by wenzelm
tuned signature;
2017-05-08, by wenzelm
tuned signature;
2017-05-08, by wenzelm
tuned signature;
2017-05-08, by wenzelm
clarified signature;
2017-05-08, by wenzelm
clarified image size;
2017-05-08, by wenzelm
proper type for iterated application;
2017-05-08, by wenzelm
make index formally within Isabelle/Scala;
2017-05-08, by wenzelm
clarified modules;
2017-05-08, by wenzelm
plot heap size;
2017-05-08, by wenzelm
more precise profiles;
2017-05-08, by wenzelm
suppress "Pure" with its special threads=1 (Jenkins log does not provide threads in ISABELLE_BUILD_OPTIONS);
2017-05-08, by wenzelm
more specific workaround (see also ed7b5cd3a7f2);
2017-05-08, by wenzelm
cpu time is somewhat redundant for threads=1;
2017-05-07, by wenzelm
clarified description vs. file name;
2017-05-07, by wenzelm
tuned output;
2017-05-07, by wenzelm
clarified types;
2017-05-07, by wenzelm
more operations;
2017-05-07, by wenzelm
more uniform charts;
2017-05-07, by wenzelm
always show ml_timing -- in another chart;
2017-05-07, by wenzelm
removed threshold: redundant due to sorting;
2017-05-07, by wenzelm
tuned output;
2017-05-07, by wenzelm
parallel gnuplot invocation;
2017-05-07, by wenzelm
more HTML output;
2017-05-07, by wenzelm
clarified explicit Build_Status.Data operations;
2017-05-07, by wenzelm
more operations;
2017-05-07, by wenzelm
more uniform threads value, notably for Pure session;
2017-05-07, by wenzelm
tuned;
2017-05-07, by wenzelm
added option verbose for SQL source;
2017-05-06, by wenzelm
merged
2017-05-06, by wenzelm
tuned signature;
2017-05-06, by wenzelm
tuned signature;
2017-05-06, by wenzelm
present build status;
2017-05-06, by wenzelm
tuned;
2017-05-06, by wenzelm
obsolete;
2017-05-06, by wenzelm
clarified name;
2017-05-06, by wenzelm
tuned messages;
2017-05-06, by wenzelm
tuned;
2017-05-06, by wenzelm
clarified signature;
2017-05-06, by wenzelm
unused;
2017-05-06, by wenzelm
tuned;
2017-05-06, by wenzelm
tuned messages;
2017-05-06, by wenzelm
performance statistics from build log database;
2017-05-06, by wenzelm
tuned;
2017-05-05, by wenzelm
legacy version for Jenkins website;
2017-05-05, by wenzelm
tuned;
2017-05-05, by wenzelm
detect database entries;
2017-05-05, by wenzelm
tuned;
2017-05-05, by wenzelm
clarified signature;
2017-05-05, by wenzelm
tuned signature;
2017-05-05, by wenzelm
NEWS: totient 1 = 1 now
2017-05-05, by Manuel Eberl
Merged
2017-05-04, by eberlm
More material on totient function
2017-05-04, by eberlm
merged
2017-05-04, by wenzelm
clarified universal view: include pull_date;
2017-05-04, by wenzelm
clarified signature: PostgreSQL manages high-volume data, SQLite only sees small snapshots;
2017-05-04, by wenzelm
clarified database layout: pull date progression follows Isabelle only, and AFP is derived from that;
2017-05-04, by wenzelm
redundant;
2017-05-04, by wenzelm
Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.jiRMht
2017-05-04, by paulson
A few more new lemmas
2017-05-04, by paulson
more permissive, e.g. for system operations as in 678e00851cfb;
2017-05-04, by wenzelm
tuned;
2017-05-04, by wenzelm
tuned;
2017-05-04, by wenzelm
prefer standard getOrElse;
2017-05-04, by wenzelm
tuned;
2017-05-04, by wenzelm
tuned;
2017-05-04, by wenzelm
more operations;
2017-05-04, by wenzelm
merged
2017-05-04, by wenzelm
clarified directory layout;
2017-05-04, by wenzelm
eliminated unused afp_pull_date table;
2017-05-04, by wenzelm
slightly more compact file;
2017-05-04, by wenzelm
produce build_log_snapshot, based on small prefix into pull_date history;
2017-05-04, by wenzelm
omit parentheses for the sake of SQLite;
2017-05-03, by wenzelm
more snapshot content;
2017-05-03, by wenzelm
more robust;
2017-05-03, by wenzelm
more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
2017-05-03, by wenzelm
tuned signature;
2017-05-03, by wenzelm
simplified: standard toString is SQL.ident;
2017-05-03, by wenzelm
tuned;
2017-05-03, by wenzelm
tuned signature;
2017-05-03, by wenzelm
clarified signature;
2017-05-03, by wenzelm
tuned signature;
2017-05-03, by wenzelm
tuned signature;
2017-05-03, by wenzelm
tuned signature;
2017-05-03, by wenzelm
clarified modules;
2017-05-03, by wenzelm
clarified pull_date tables;
2017-05-03, by wenzelm
views for full PostgreSQL database;
2017-05-02, by wenzelm
eliminated redundant type SQL.View;
2017-05-02, by wenzelm
tuned;
2017-05-02, by wenzelm
tuned signature;
2017-05-02, by wenzelm
tuned;
2017-05-02, by wenzelm
two new theorems
2017-05-03, by paulson
merged
2017-05-02, by wenzelm
detect old log files (early 2016);
2017-05-02, by wenzelm
explicit support for multiple regexes;
2017-05-02, by wenzelm
some derived data fields, to facilitate queries;
2017-05-02, by wenzelm
tuned signature;
2017-05-02, by wenzelm
Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.VldMQI
2017-05-02, by paulson
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-05-02, by paulson
more general pattern;
2017-05-02, by wenzelm
more timing;
2017-05-02, by wenzelm
proper quote (amending 546020a98a91): e.g. relevant for "ISABELLE_BUILD_OPTIONS";
2017-05-02, by wenzelm
suppress build_log_snapshot: too bulky;
2017-05-02, by wenzelm
more Jenkins logs for build_log database;
2017-05-01, by wenzelm
approximate repository identify job based on isabelle-nightly-slow;
2017-05-01, by wenzelm
tuned;
2017-05-01, by wenzelm
tuned signature;
2017-05-01, by wenzelm
clarified treatment of qualified names (amending 7ef438495a02);
2017-05-01, by wenzelm
create full view on build_log data, but avoid bombing sqlitebrowser;
2017-05-01, by wenzelm
support for views;
2017-05-01, by wenzelm
more operations;
2017-05-01, by wenzelm
slightly more compact file;
2017-05-01, by wenzelm
incremental download of Jenkins log files, which are also added to database;
2017-05-01, by wenzelm
more robust detection of Jenkins log;
2017-05-01, by wenzelm
detect Jenkins log files as well;
2017-05-01, by wenzelm
detect host name;
2017-05-01, by wenzelm
more parallelism;
2017-05-01, by wenzelm
tuned;
2017-05-01, by wenzelm
proper log_path check;
2017-05-01, by wenzelm
ensure canonical order: latest first;
2017-05-01, by wenzelm
tuned signature;
2017-05-01, by wenzelm
download Jenkins logs with inlined ml_statistics;
2017-05-01, by wenzelm
tuned;
2017-05-01, by wenzelm
clarified signature;
2017-05-01, by wenzelm
tuned signature;
2017-05-01, by wenzelm
read ml_statistics from session logs: .db or .gz files;
2017-05-01, by wenzelm
more informative log_filename;
2017-05-01, by wenzelm
retrieve more than just 100 builds;
2017-04-30, by wenzelm
clarified modules;
2017-04-30, by wenzelm
tuned signature;
2017-04-30, by wenzelm
tuned signature;
2017-04-30, by wenzelm
clarified database update: full ml_statistics on server, no ml_statistics on plain file;
2017-04-30, by wenzelm
parse ml_statistics only when required;
2017-04-30, by wenzelm
clarified database layout: bulky ml_statistics are stored/retrieved separately;
2017-04-30, by wenzelm
support for qualified names, which are not quoted (e.g. for SQLite);
2017-04-30, by wenzelm
clarified dummy Session_Entry;
2017-04-30, by wenzelm
clarified database update operations;
2017-04-30, by wenzelm
tuned message;
2017-04-30, by wenzelm
maintain build_log database;
2017-04-29, by wenzelm
exclude special log files;
2017-04-29, by wenzelm
tuned;
2017-04-29, by wenzelm
tuned;
2017-04-29, by wenzelm
ssh_close for proper termination after use of database;
2017-04-29, by wenzelm
some documentation;
2017-04-29, by wenzelm
merged
2017-04-29, by wenzelm
tuned;
2017-04-29, by wenzelm
tuned signature;
2017-04-29, by wenzelm
clarified database content;
2017-04-29, by wenzelm
more operations;
2017-04-29, by wenzelm
optional ml_statistics: much faster;
2017-04-29, by wenzelm
proper query (amending ce15da15f8e2);
2017-04-29, by wenzelm
put bulky data last;
2017-04-29, by wenzelm
tuned;
2017-04-29, by wenzelm
more log files;
2017-04-29, by wenzelm
clarified multi-line properties;
2017-04-29, by wenzelm
dummy session entry for empty build_info: relevant for filter_files;
2017-04-28, by wenzelm
tuned query, notably for isabelle_build_log_build_info;
2017-04-28, by wenzelm
operations to read database;
2017-04-28, by wenzelm
tuned signature: less overloading;
2017-04-28, by wenzelm
tuned signature;
2017-04-28, by wenzelm
tuned transaction granularity;
2017-04-28, by wenzelm
unused;
2017-04-28, by wenzelm
clarified database layout;
2017-04-28, by wenzelm
tuned signature: avoid null in regular Scala code;
2017-04-28, by wenzelm
clarified transaction boundaries: more robust incremental write operations;
2017-04-28, by wenzelm
clarified database layout;
2017-04-28, by wenzelm
allow null for primitive types;
2017-04-28, by wenzelm
more uniform storage of Meta_Info;
2017-04-28, by wenzelm
allow null;
2017-04-28, by wenzelm
clarified plain_name / log_name;
2017-04-28, by wenzelm
tuned comment;
2017-04-28, by wenzelm
tuned signature;
2017-04-28, by wenzelm
tuned;
2017-04-28, by wenzelm
separate small meta_info vs. big build_info;
2017-04-28, by wenzelm
tuned;
2017-04-28, by wenzelm
unused;
2017-04-28, by wenzelm
tuned signature;
2017-04-28, by wenzelm
more standard multi-line storage in database: Prop.separator is only required for single-line meta_info within log file;
2017-04-28, by wenzelm
clarified filter_files: sorted and unique;
2017-04-28, by wenzelm
database storage of Meta_Info and Build_Info;
2017-04-28, by wenzelm
allow null;
2017-04-27, by wenzelm
more encode/decode operations;
2017-04-27, by wenzelm
proper prefix;
2017-04-27, by wenzelm
support for database connection;
2017-04-27, by wenzelm
clarified treatment of default port;
2017-04-27, by wenzelm
tuned signature;
2017-04-27, by wenzelm
clarified modules;
2017-04-27, by wenzelm
more SQL operations;
2017-04-27, by wenzelm
more robust (see also 6688b9cd443b);
2017-04-26, by wenzelm
more robust treatment of non-UTF8 text files (cf. 3ed43cfc8b14), notably old log files in ISO-8859-15;
2017-04-26, by wenzelm
clarified signature;
2017-04-26, by wenzelm
New material (and some tidying) purely in the Analysis directory
2017-04-27, by paulson
Merge
2017-04-27, by paulson
Some fixes related to compactE_image
2017-04-26, by paulson
Merge
2017-04-26, by paulson
Further new material. The simprule status of some exp and ln identities was reverted.
2017-04-26, by paulson
tuned Approximation: separated general material from oracle
2017-04-26, by eberlm
better code equation for binomial
2017-04-26, by eberlm
meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;
2017-04-25, by wenzelm
Fixed LaTeX issue
2017-04-25, by paulson
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-04-25, by paulson
instance for polynomial rings with characteristic zero
2017-04-25, by haftmann
recovered document from 0f3fdf689bf9;
2017-04-24, by wenzelm
tuned;
2017-04-24, by wenzelm
clarified parent session images, to avoid duplicate loading of theories;
2017-04-24, by wenzelm
clarified parent session images, to avoid duplicate loading of theories;
2017-04-24, by wenzelm
clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;
2017-04-24, by wenzelm
clarified modules;
2017-04-24, by wenzelm
actually use theory;
2017-04-23, by wenzelm
clarified parent session images, to avoid duplicate loading of theories;
2017-04-23, by wenzelm
merged
2017-04-23, by wenzelm
tuned documentation;
2017-04-23, by wenzelm
support for potential session imports;
2017-04-23, by wenzelm
more checks;
2017-04-23, by wenzelm
tuned messages;
2017-04-23, by wenzelm
actually use theory;
2017-04-23, by wenzelm
renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
2017-04-23, by wenzelm
support for Mercurial manifest check;
2017-04-23, by wenzelm
tuned;
2017-04-23, by wenzelm
more operations;
2017-04-23, by wenzelm
support for multiple operations via options;
2017-04-23, by wenzelm
clarified tool name -- more official status;
2017-04-23, by wenzelm
more lemmas
2017-04-23, by haftmann
include GCD as integral part of computational algebra in session HOL
2017-04-23, by haftmann
prefer strict operation (despite 8edca3465758): there might be errors from all_known = true (ae09b9f5980b);
2017-04-23, by wenzelm
added missing file (amending f533820e7248);
2017-04-23, by wenzelm
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2017-04-22, by wenzelm
merged
2017-04-22, by wenzelm
clarified parent session images, to avoid duplicate loading of theories;
2017-04-22, by wenzelm
tuned;
2017-04-21, by wenzelm
removed pointless document;
2017-04-21, by wenzelm
moved lemmas from AFP to Isabelle
2017-04-21, by blanchet
moved lemmas from AFP to Isabelle
2017-04-21, by blanchet
two new induction principles on multisets
2017-04-21, by blanchet
merged
2017-04-21, by wenzelm
clarified session imports;
2017-04-21, by wenzelm
clarified standard_import: based on Known.get_file as in PIDE editors;
2017-04-21, by wenzelm
afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
2017-04-21, by wenzelm
proper imports_resources for import_name: avoid self-referential name resolution;
2017-04-21, by wenzelm
more precise position information;
2017-04-21, by wenzelm
tuned imports;
2017-04-21, by wenzelm
proper "~~" backup as documented;
2017-04-21, by wenzelm
clarified: explicit check of result;
2017-04-21, by wenzelm
clarified imports;
2017-04-21, by wenzelm
clarified local_theories: exclude ancestor sessions;
2017-04-21, by wenzelm
more standard master_dir;
2017-04-21, by wenzelm
eliminated default_qualifier: just a constant;
2017-04-21, by wenzelm
more uniform isabelle_scala;
2017-04-21, by wenzelm
include imports that morally belong to Main and are used in HOL-Proofs applications;
2017-04-21, by wenzelm
tuned;
2017-04-21, by wenzelm
proper theory_qualifier;
2017-04-21, by wenzelm
more global theories;
2017-04-20, by wenzelm
actual update_imports operations;
2017-04-20, by wenzelm
more operations;
2017-04-20, by wenzelm
tuned signature;
2017-04-20, by wenzelm
more operations;
2017-04-20, by wenzelm
tuned signature;
2017-04-20, by wenzelm
tuned whitespace;
2017-04-20, by wenzelm
clarified;
2017-04-20, by wenzelm
store Sessions.Info.name;
2017-04-20, by wenzelm
wrapper for "isabelle update_imports" with selection options like "isabelle build";
2017-04-19, by wenzelm
more position information;
2017-04-19, by wenzelm
removed French accent from docs
2017-04-20, by blanchet
removed Old_SMT legacy module
2017-04-20, by blanchet
typo
2017-04-20, by nipkow
tuned imports;
2017-04-19, by wenzelm
always explore all sessions;
2017-04-19, by wenzelm
optionally explore all sessions -- potentially slow, e.g. for AFP;
2017-04-19, by wenzelm
proper sections;
2017-04-19, by wenzelm
clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
2017-04-19, by wenzelm
proper base name, e.g. relevant for Code_Namespace.hierarchical_program;
2017-04-19, by wenzelm
clarified session graph: collapse theories from other sessions;
2017-04-18, by wenzelm
more robust error (amending 2c27c3d1fd3b): responsibility is gradually moved from ML to Scala;
2017-04-18, by wenzelm
exclude theories from other sessions;
2017-04-18, by wenzelm
some documentation;
2017-04-18, by wenzelm
actually qualify theory names;
2017-04-18, by wenzelm
merged
2017-04-17, by wenzelm
prefer formal name from session context, for proper qualified theory name;
2017-04-17, by wenzelm
clarified: Map index uses canonical files;
2017-04-17, by wenzelm
tuned signature;
2017-04-17, by wenzelm
tuned signature;
2017-04-17, by wenzelm
uniform use of theory base name for presentation;
2017-04-17, by wenzelm
proper imports_base, notably for thy_deps;
2017-04-17, by wenzelm
tuned signature;
2017-04-17, by wenzelm
tuned;
2017-04-17, by wenzelm
tuned GUI;
2017-04-17, by wenzelm
obsolete;
2017-04-17, by wenzelm
more uniform thy_deps (like class_deps), see also c48d536231fe;
2017-04-17, by wenzelm
special theories are always global;
2017-04-17, by wenzelm
tuned signature;
2017-04-17, by wenzelm
tuned signature;
2017-04-17, by wenzelm
tuned signature;
2017-04-17, by wenzelm
more systematic treatment of polynomial 1
2017-04-17, by haftmann
consistent session name
2017-04-17, by haftmann
more rules concerning of_nat, of_int, numeral
2017-04-16, by haftmann
for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
2017-04-13, by haftmann
early abort on depth limit
2017-04-13, by haftmann
obsolete
2017-04-13, by haftmann
tuned
2017-04-13, by haftmann
merged
2017-04-13, by wenzelm
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
2017-04-13, by wenzelm
clarified directories;
2017-04-13, by wenzelm
tuned signature (again);
2017-04-13, by wenzelm
proper bootstrap base for building Pure;
2017-04-12, by wenzelm
tuned according to Scala version;
2017-04-12, by wenzelm
more global theories;
2017-04-12, by wenzelm
tuned;
2017-04-12, by wenzelm
clarified loaded_theories: map to qualified theory name;
2017-04-12, by wenzelm
global session_base for PIDE interaction;
2017-04-12, by wenzelm
more explicit jEdit file operations;
2017-04-12, by wenzelm
early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;
2017-04-12, by wenzelm
tuned;
2017-04-12, by wenzelm
tuned
2017-04-12, by haftmann
more fundamental euler's totient function on nat rather than int;
2017-04-12, by haftmann
merged
2017-04-12, by wenzelm
more informative known_files: known_theories within the local session directory come first;
2017-04-11, by wenzelm
less global theories -- conflict with AFP entries;
2017-04-11, by wenzelm
support for known theories files (according to multiple uses);
2017-04-11, by wenzelm
proper display_name;
2017-04-10, by wenzelm
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
2017-04-10, by wenzelm
tuned signature;
2017-04-10, by wenzelm
proper import qualifier for global theories;
2017-04-10, by wenzelm
explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
2017-04-10, by wenzelm
proper qualifier for imports;
2017-04-10, by wenzelm
clarified, according to Scala version;
2017-04-10, by wenzelm
tuned text;
2017-04-10, by wenzelm
clarified signature;
2017-04-10, by wenzelm
NEWS;
2017-04-09, by wenzelm
more robust: user could provide name with "/" etc.;
2017-04-09, by wenzelm
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
2017-04-09, by wenzelm
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
2017-04-09, by wenzelm
clarified main CTT.thy, and avoid name clash with global HOL/Main.thy;
2017-04-09, by wenzelm
tuned signature -- prefer qualified names;
2017-04-09, by wenzelm
more qualifier treatment, but in the end it is still ignored;
2017-04-08, by wenzelm
tuned signature;
2017-04-08, by wenzelm
provide Resources.import_name in ML, similar to Scala version;
2017-04-08, by wenzelm
clarified;
2017-04-08, by wenzelm
more session_base information in ML;
2017-04-08, by wenzelm
more operations;
2017-04-08, by wenzelm
tuned signature;
2017-04-08, by wenzelm
merged
2017-04-11, by nipkow
doc for comp. ind.
2017-04-11, by nipkow
tuned signature
2017-04-10, by traytel
tuned headers;
2017-04-07, by wenzelm
merged
2017-04-07, by wenzelm
refer to known_theory;
2017-04-07, by wenzelm
tuned;
2017-04-07, by wenzelm
provide session base for "isabelle build" and "isabelle console" ML process;
2017-04-07, by wenzelm
tuned comment;
2017-04-07, by wenzelm
more explicit lookup of loaded_theories: base names allowed here;
2017-04-07, by wenzelm
support for all_known_theories of all sessions;
2017-04-07, by wenzelm
tuned;
2017-04-07, by wenzelm
known_theories from imported sessions;
2017-04-07, by wenzelm
tuned;
2017-04-07, by wenzelm
more checks;
2017-04-07, by wenzelm
tuned;
2017-04-07, by wenzelm
tuned signature;
2017-04-07, by wenzelm
tuned;
2017-04-07, by wenzelm
support for static session imports, without affect build hierarchy;
2017-04-07, by wenzelm
explicit Sessions.Selection;
2017-04-07, by wenzelm
more general signature; works for all terms, not just frees
2017-04-07, by Lars Hupel
session containing computational algebra
2017-04-06, by haftmann
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
2017-04-06, by haftmann
clarified signature: tree structure is not essential;
2017-04-06, by wenzelm
merged
2017-04-06, by wenzelm
misc tuning and modernization;
2017-04-06, by wenzelm
merged
2017-04-06, by Lars Hupel
use Item_Net to store inductive info
2017-04-05, by Lars Hupel
tuned whitespace;
2017-04-06, by wenzelm
tuned signature;
2017-04-06, by wenzelm
more accurate qualified lookup;
2017-04-06, by wenzelm
clarified fall-back name;
2017-04-06, by wenzelm
tuned signature;
2017-04-06, by wenzelm
tuned whitespace;
2017-04-06, by wenzelm
clarified modules;
2017-04-06, by wenzelm
clarified checks -- avoid duplicated messages (amending 60c159d490a2);
2017-04-06, by wenzelm
proper default (amending 601866c61ded);
2017-04-06, by wenzelm
Fixed import path in Factorial_Ring
2017-04-06, by eberlm
Merged
2017-04-06, by eberlm
Merged
2017-04-06, by eberlm
Tuned
2017-04-04, by eberlm
Merged
2017-04-04, by eberlm
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
2017-04-04, by eberlm
moved material from AFP to distribution
2017-04-04, by eberlm
merged
2017-04-05, by wenzelm
misc tuning and modernization;
2017-04-05, by wenzelm
uniform import_name, with treatment of global and qualified theories;
2017-04-05, by wenzelm
tuned signature;
2017-04-05, by wenzelm
more concise criterion
2017-04-05, by haftmann
tuned
2017-04-05, by haftmann
more on lists
2017-04-05, by haftmann
store totality fact in function info
2017-04-05, by Lars Hupel
allow to load this into "isabelle jedit -l HOL";
2017-04-04, by wenzelm
print like syntax of Thy_Header.header;
2017-04-04, by wenzelm
more explicit types;
2017-04-04, by wenzelm
proper name according to meaning;
2017-04-04, by wenzelm
more main sessions and global theories;
2017-04-04, by wenzelm
eliminated redundant imports;
2017-04-04, by wenzelm
eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
2017-04-04, by wenzelm
tuned (see also 1fa1023b13b9);
2017-04-04, by wenzelm
tuned header;
2017-04-04, by wenzelm
tuned signature;
2017-04-04, by wenzelm
proper base name;
2017-04-04, by wenzelm
tuned;
2017-04-04, by wenzelm
tuned syntax;
2017-04-04, by wenzelm
clarified: allow to qualify theories from ROOT;
2017-04-04, by wenzelm
refer to global_theories from all sessions, before selection;
2017-04-04, by wenzelm
tuned signature;
2017-04-04, by wenzelm
tuned;
2017-04-04, by wenzelm
macbroy30 is on 10.12 Sierra (already since 04-Mar-2017) -- discontinued support for 10.8 Mountain Lion;
2017-04-04, by wenzelm
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
2017-04-04, by wenzelm
tuned headers;
2017-04-04, by wenzelm
proper imports;
2017-04-04, by wenzelm
tuned message;
2017-04-03, by wenzelm
merged
2017-04-03, by wenzelm
misc tuning and modernization;
2017-04-03, by wenzelm
clarified imports;
2017-04-03, by wenzelm
tuned signature;
2017-04-03, by wenzelm
tuned;
2017-04-03, by wenzelm
provide session qualifier via resources;
2017-04-03, by wenzelm
proper qualifier (again, see df4cd6e1fdfa);
2017-04-03, by wenzelm
simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);
2017-04-03, by wenzelm
tuned;
2017-04-03, by wenzelm
tuned signature;
2017-04-03, by wenzelm
removed problematic simp rule
2017-04-03, by eberlm
merged
2017-04-03, by nipkow
tuned
2017-04-03, by nipkow
Merged
2017-04-03, by eberlm
added shuffle product to HOL/List
2017-04-03, by eberlm
tuned
2017-04-03, by nipkow
added chains of (in)equations
2017-04-03, by nipkow
misc tuning and modernization;
2017-04-01, by wenzelm
misc tuning and modernization;
2017-04-01, by wenzelm
clarified YXML vs. symbol encoding: operate on whole message;
2017-04-01, by wenzelm
clarified YXML vs. symbol encoding: operate on whole message;
2017-04-01, by wenzelm
tuned proofs;
2017-04-01, by wenzelm
misc tuning and modernization;
2017-04-01, by wenzelm
tuned signature;
2017-04-01, by wenzelm
tuned
2017-04-01, by nipkow
more lemmas
2017-03-31, by nipkow
tuned proof;
2017-03-23, by wenzelm
merged
2017-03-20, by wenzelm
misc tuning and modernization;
2017-03-20, by wenzelm
support to encode/decode command state;
2017-03-20, by wenzelm
tuned;
2017-03-20, by wenzelm
more operations;
2017-03-20, by wenzelm
tuned signature;
2017-03-20, by wenzelm
eliminated redundant check (see also 27328dcaf64c vs. 9c53198dbb1c);
2017-03-20, by wenzelm
Corrected affiliation.
2017-03-20, by ballarin
updated to jedit-5.4.0;
2017-03-19, by wenzelm
misc tuning and modernization;
2017-03-19, by wenzelm
clarified signature: rowid is specific to SQLite;
2017-03-19, by wenzelm
proper primary key;
2017-03-19, by wenzelm
more general primary_key;
2017-03-19, by wenzelm
tuned;
2017-03-19, by wenzelm
more operations;
2017-03-19, by wenzelm
tuned;
2017-03-19, by wenzelm
proper SQL syntax (according of PostgreSQL);
2017-03-19, by wenzelm
access table via session_name: db may in principle contain multiple entries;
2017-03-19, by wenzelm
more operations;
2017-03-19, by wenzelm
eliminated somewhat redundant inlined name (despite a7aa17a1f721);
2017-03-19, by wenzelm
more informative session result;
2017-03-18, by wenzelm
simplified signature (despite 448325de6e4f);
2017-03-18, by wenzelm
clarified signature;
2017-03-18, by wenzelm
tuned;
2017-03-18, by wenzelm
more realistic PIDE build session;
2017-03-18, by wenzelm
more uniform options;
2017-03-18, by wenzelm
asynchronous send_stop operation;
2017-03-18, by wenzelm
more process arguments;
2017-03-18, by wenzelm
proper message text (see also fa62e095d8f1);
2017-03-18, by wenzelm
support PIDE option (inactive);
2017-03-18, by wenzelm
more explicit build_session args;
2017-03-18, by wenzelm
avoid compiler warning;
2017-03-18, by wenzelm
actually throw exception;
2017-03-18, by wenzelm
clarified result;
2017-03-18, by wenzelm
reset print_mode, e.g. relevant for saved heap;
2017-03-18, by wenzelm
clarified init (see also 32755e357a51, ac48def96b69);
2017-03-18, by wenzelm
restore output channels after shutdown, e.g. relevant for saved heap;
2017-03-18, by wenzelm
clarified signature;
2017-03-18, by wenzelm
merged
2017-03-17, by wenzelm
tuned;
2017-03-17, by wenzelm
proper columns;
2017-03-17, by wenzelm
tuned signature;
2017-03-17, by wenzelm
more general signature: not limited to SQLite;
2017-03-17, by wenzelm
suppress inlined properties from log output;
2017-03-17, by wenzelm
prefer database, but also accept log.gz from historic versions;
2017-03-17, by wenzelm
more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;
2017-03-17, by wenzelm
maintain persistent session info in SQLite database instead of log file;
2017-03-17, by wenzelm
tuned;
2017-03-17, by wenzelm
tuned signature;
2017-03-17, by wenzelm
tuned;
2017-03-17, by wenzelm
tuned message;
2017-03-17, by wenzelm
clarified signature;
2017-03-17, by wenzelm
more selective queries;
2017-03-17, by wenzelm
clarified data representation;
2017-03-17, by wenzelm
data representation with XML.Cache;
2017-03-17, by wenzelm
clarified name;
2017-03-17, by wenzelm
SQL database operations for combined session info;
2017-03-16, by wenzelm
prefer non-strict default;
2017-03-16, by wenzelm
clarified signature (again, see also 3ed43cfc8b14);
2017-03-16, by wenzelm
tuned signature;
2017-03-16, by wenzelm
tuned;
2017-03-16, by wenzelm
tuned comments;
2017-03-16, by wenzelm
clarified message: exception output usally happens in a context without extra newline;
2017-03-16, by wenzelm
Removed [simp] status for Complex_eq. Also tidied some proofs
2017-03-16, by paulson
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
2017-03-16, by paulson
always output proof state: there is only one output buffer in Isabelle/VSCode;
2017-03-15, by wenzelm
updated package;
2017-03-15, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
tip