isabelle: Graph

tuned;
2018-01-08, by wenzelm
moved in some material from Euler-MacLaurin
2018-01-08, by paulson
merged
2018-01-07, by wenzelm
prefer formal comments;
2018-01-07, by wenzelm
clarified NEWS;
2018-01-07, by wenzelm
tuned whitespace;
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
support for formal comments in ML in Isabelle/Scala;
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
tuned message;
2018-01-07, by wenzelm
allow formal comments in ML;
2018-01-07, by wenzelm
clarified modules;
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
more uniform output: formal comments within {* ... *};
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
clarified output: avoid extra space;
2018-01-07, by wenzelm
output token content with formal comments and antiquotations;
2018-01-07, by wenzelm
tuned;
2018-01-07, by wenzelm
clarified signature;
2018-01-06, by wenzelm
clarified modules;
2018-01-06, by wenzelm
inner syntax comments may be written as "\<comment> \<open>text\<close>";
2018-01-06, by wenzelm
spelling
2018-01-07, by haftmann
corrected op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op's
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op
2018-01-06, by nipkow
tuned op's
2018-01-05, by nipkow
Renamed (^) to [^] in preparation of the move from "op X" to (X)
2018-01-05, by nipkow
tuned op
2018-01-05, by nipkow
HOL-Analysis: add set_integrable_restrict_space
2018-01-04, by hoelzl
more correct parentheses
2018-01-03, by haftmann
more tight HTML output: avoid extra lines within <pre>;
2018-01-03, by wenzelm
HTML output for Markdown elements;
2018-01-03, by wenzelm
updated NEWS
2018-01-03, by blanchet
removed dead code
2018-01-03, by blanchet
removed old 'add_datatype' ML functions
2018-01-03, by blanchet
kill old size infrastructure
2018-01-03, by blanchet
repaired whitespace accident from 2505cabfc515
2018-01-02, by haftmann
proper namespace for evaluators
2018-01-01, by haftmann
tuned
2018-01-01, by haftmann
more correct name resolving
2018-01-01, by haftmann
skip abstract constructors silently in datatype clauses of computations
2018-01-01, by haftmann
removed para about 'old_datatype' in docs
2018-01-02, by blanchet
old_datatype no longer exists (cf. 706b1cf7b76d);
2018-01-02, by wenzelm
merged
2018-01-02, by wenzelm
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
2018-01-02, by wenzelm
clarified terminology of "markdown_bullet";
2018-01-02, by wenzelm
compile
2018-01-02, by blanchet
updated dependencies + compile
2018-01-02, by blanchet
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
2018-01-02, by blanchet
removed 'old_datatype' command
2018-01-02, by blanchet
don't test 'old_datatype', which is on its way out
2018-01-02, by blanchet
ported inductive realizer to new datatype package
2018-01-02, by blanchet
removed needless theorems
2018-01-02, by blanchet
store high-level 'size' equations
2018-01-02, by blanchet
avoid call to function that may throw an exception in error message
2018-01-02, by blanchet
misc tuning and modernization;
2018-01-01, by wenzelm
more completion templates;
2018-01-01, by wenzelm
proper purge of auxiliary bibtex theory;
2018-01-01, by wenzelm
tuned signature;
2018-01-01, by wenzelm
tuned;
2018-01-01, by wenzelm
Restored correct spacing for set comprehensions
2017-12-31, by paulson
less redundant;
2017-12-30, by wenzelm
more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
2017-12-30, by wenzelm
more robust treatment of conflicts with existing Unicode text;
2017-12-30, by wenzelm
tuned whitespace;
2017-12-30, by wenzelm
no check for bibtex entries from other sessions;
2017-12-29, by wenzelm
clarified signature;
2017-12-29, by wenzelm
more accurate message patterns;
2017-12-29, by wenzelm
prefer formal citations;
2017-12-29, by wenzelm
proper bibtex entries;
2017-12-29, by wenzelm
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
2017-12-29, by wenzelm
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
2017-12-28, by wenzelm
NEWS;
2017-12-28, by wenzelm
proper check for imports, not just ROOT entries;
2017-12-28, by wenzelm
tuned signature;
2017-12-28, by wenzelm
implicit thy_load context for bibtex files (VSCode);
2017-12-28, by wenzelm
bibtex theory is always required and thus eventually consolidated;
2017-12-28, by wenzelm
implicit thy_load context for bibtex files;
2017-12-28, by wenzelm
clarified signature: prefer Document.Node.Name.is_bibtex;
2017-12-28, by wenzelm
avoid spurious noise: Prover IDE is meant to check for errors;
2017-12-28, by wenzelm
clarified signature;
2017-12-28, by wenzelm
avoid clash with special files in HTML output;
2017-12-28, by wenzelm
unused;
2017-12-28, by wenzelm
tuned signature;
2017-12-28, by wenzelm
prefer existing Resources.check_path;
2017-12-28, by wenzelm
more accurate bibtex entries;
2017-12-28, by wenzelm
added command 'bibtex_file' (for PIDE interaction only);
2017-12-28, by wenzelm
clarified default position for empty message pos;
2017-12-27, by wenzelm
spelling
2017-12-25, by haftmann
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
2017-12-24, by eberlm
fewer warnings;
2017-12-24, by wenzelm
clarified positions;
2017-12-24, by wenzelm
check bibtex database on ML side -- for semantic PIDE editing;
2017-12-24, by wenzelm
clarified directories;
2017-12-24, by wenzelm
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
2017-12-24, by wenzelm
check bibtex database: errors and warnings;
2017-12-23, by wenzelm
more symbols;
2017-12-23, by wenzelm
Merge
2017-12-22, by paulson
Merge
2017-12-22, by paulson
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
2017-12-22, by paulson
more symbols;
2017-12-22, by wenzelm
tuned;
2017-12-22, by wenzelm
store full blob source for the sake of markup_to_XML;
2017-12-22, by wenzelm
PIDE markup for non-theory nodes;
2017-12-22, by wenzelm
discontinued 'display_drafts' command;
2017-12-22, by wenzelm
action "isabelle.draft" for plain-text preview;
2017-12-22, by wenzelm
NEWS;
2017-12-22, by wenzelm
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
2017-12-22, by wenzelm
tuned;
2017-12-22, by wenzelm
clarified URL: unique node name;
2017-12-22, by wenzelm
clarified signature;
2017-12-22, by wenzelm
proper title;
2017-12-22, by wenzelm
HTML rendering of \<^control> as in Isabelle/jEdit;
2017-12-22, by wenzelm
auto update;
2017-12-22, by wenzelm
clarified modules;
2017-12-22, by wenzelm
proper HTML title;
2017-12-22, by wenzelm
tuned signature;
2017-12-22, by wenzelm
tuned output;
2017-12-21, by wenzelm
merged
2017-12-21, by wenzelm
isabelle.preview presents bibtex database files as well;
2017-12-21, by wenzelm
clarified signature;
2017-12-21, by wenzelm
isabelle.preview presents auxiliary text files as well;
2017-12-21, by wenzelm
tuned signature;
2017-12-21, by wenzelm
tuned signature;
2017-12-21, by wenzelm
bibtex HTML output via external tool;
2017-12-21, by wenzelm
merged
2017-12-21, by nipkow
tuned op's
2017-12-21, by nipkow
tuned op's
2017-12-21, by nipkow
tuned op's
2017-12-21, by nipkow
tuned op's
2017-12-21, by nipkow
tuned op's
2017-12-21, by nipkow
tuned op's
2017-12-21, by nipkow
tuned;
2017-12-21, by wenzelm
Some lemmas on complex numbers and coprimality
2017-12-21, by eberlm
merged
2017-12-20, by nipkow
tuned op's
2017-12-20, by nipkow
tuned op's
2017-12-20, by nipkow
tuned op's
2017-12-20, by nipkow
tuned op's
2017-12-20, by nipkow
tuned op's
2017-12-20, by nipkow
updated URL;
2017-12-20, by wenzelm
isabelle update_cartouches -c -t;
2017-12-19, by wenzelm
have 'try0' display results faster
2017-12-19, by blanchet
a conditional paramitrecity prover
2017-12-18, by traytel
removed debug output
2017-12-18, by traytel
made tactics more robust
2017-12-17, by traytel
tuned;
2017-12-16, by wenzelm
more markup;
2017-12-16, by wenzelm
added document antiquotation @{session name};
2017-12-16, by wenzelm
more accurate parse_nat/parse_int: avoid corner cases of Int.fromString (e.g. "1.0");
2017-12-16, by wenzelm
tuned;
2017-12-16, by wenzelm
disallow theory name "ROOT";
2017-12-16, by wenzelm
PIDE markup for session ROOT files;
2017-12-16, by wenzelm
tuned;
2017-12-16, by wenzelm
more operations;
2017-12-16, by wenzelm
tuned;
2017-12-16, by wenzelm
recovered Options.default_markup, e.g. for src/Doc/antiquote_setup.ML (amending 16519cd83ed4);
2017-12-16, by wenzelm
tuned;
2017-12-16, by wenzelm
clarified signature;
2017-12-16, by wenzelm
clarified signature;
2017-12-16, by wenzelm
dedicated case option for code generation to Scala
2017-12-14, by haftmann
minor performance tuning, notably for Library.fold_string etc.;
2017-12-14, by wenzelm
clarified file name;
2017-12-14, by wenzelm
purge log files -- avoid old errors;
2017-12-14, by wenzelm
expose bibtex errors;
2017-12-14, by wenzelm
proper exception;
2017-12-14, by wenzelm
proper \isakeeptag (amending 13b5c3ff1954);
2017-12-14, by wenzelm
tuned;
2017-12-14, by wenzelm
NEWS;
2017-12-14, by wenzelm
merged
2017-12-14, by wenzelm
purge more carefully (amending 26f548370e8d);
2017-12-13, by wenzelm
more error information according to @<Print type of token list@> in pdfweb.tex;
2017-12-13, by wenzelm
avoid redundant positions;
2017-12-13, by wenzelm
positions as postlude: avoid intrusion of odd %-forms into main tex source;
2017-12-13, by wenzelm
scan only one line, for more detailed positions;
2017-12-12, by wenzelm
purge more thoroughly;
2017-12-12, by wenzelm
option document_positions;
2017-12-12, by wenzelm
clarified file pattern;
2017-12-12, by wenzelm
ensure separation of TeX tokens;
2017-12-12, by wenzelm
simplified positions -- line is also human-readable in generated .tex file;
2017-12-12, by wenzelm
tuned message;
2017-12-12, by wenzelm
avoid excessive whitespace between antiquotations and text;
2017-12-12, by wenzelm
updated documentation;
2017-12-11, by wenzelm
more robust range on preceding comment-line;
2017-12-11, by wenzelm
proper file;
2017-12-11, by wenzelm
clarified file positions;
2017-12-11, by wenzelm
more operations;
2017-12-11, by wenzelm
tuned messages;
2017-12-10, by wenzelm
clean log file on Windows;
2017-12-10, by wenzelm
avoid println with its extra CR on Windows;
2017-12-10, by wenzelm
removed obsolete option (see 74a1b722507e);
2017-12-10, by wenzelm
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
2017-12-10, by wenzelm
removed Emacs legacy;
2017-12-10, by wenzelm
more robust Windows support;
2017-12-10, by wenzelm
more explicit latex errors;
2017-12-10, by wenzelm
some support for LaTeX;
2017-12-08, by wenzelm
added lemmas
2017-12-13, by nipkow
added min_list and arg_min_list
2017-12-13, by nipkow
made arg_min_on definition
2017-12-13, by nipkow
added lemmas
2017-12-13, by nipkow
Moved analysis material from AFP
2017-12-12, by Manuel Eberl
Some facts on the Mangoldt function
2017-12-11, by eberlm
dedicated theory for group closure
2017-12-08, by haftmann
clarified error;
2017-12-08, by wenzelm
removed somewhat pointless warning;
2017-12-08, by wenzelm
uniform use of original theory;
2017-12-08, by wenzelm
implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
2017-12-08, by wenzelm
avoid smt proofs in distribution
2017-12-07, by haftmann
more robust;
2017-12-07, by wenzelm
merged
2017-12-07, by wenzelm
clarified document preparation vs. skip_proofs;
2017-12-07, by wenzelm
"important" annotations
2017-12-07, by nipkow
canonical name
2017-12-07, by nipkow
tuned output in isar-ref manual;
2017-12-07, by wenzelm
obsolete (used to be part of old src/Pure/codegen.ML);
2017-12-07, by wenzelm
just one session for bulky HOL-Analysis documents;
2017-12-06, by wenzelm
more default tags;
2017-12-06, by wenzelm
merged
2017-12-06, by wenzelm
prefer control symbol antiquotations;
2017-12-06, by wenzelm
more robust, e.g. when Sidekick produces multi-selection;
2017-12-06, by wenzelm
prefer control symbol antiquotations;
2017-12-06, by wenzelm
more embedded cartouche arguments;
2017-12-06, by wenzelm
name mangling for Latex macros;
2017-12-06, by wenzelm
removed (un)important tags again to make latex happy
2017-12-06, by nipkow
initial version of Analysis document
2017-12-06, by nipkow
tuned
2017-12-06, by nipkow
merged
2017-12-05, by wenzelm
more documentation;
2017-12-05, by wenzelm
explicit tag for document commands: avoid implicit use of document_tags;
2017-12-05, by wenzelm
system option for default command tags;
2017-12-05, by wenzelm
tuned;
2017-12-05, by wenzelm
tuned signature;
2017-12-05, by wenzelm
Moved material from AFP to Analysis/Number_Theory
2017-12-05, by Manuel Eberl
merged
2017-12-04, by wenzelm
NEWS;
2017-12-04, by wenzelm
added action to make antiquoted cartouche;
2017-12-04, by wenzelm
tuned signature;
2017-12-04, by wenzelm
tuned signature;
2017-12-04, by wenzelm
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
2017-12-04, by wenzelm
clarified control style;
2017-12-04, by wenzelm
font style for literal control symbols, notably for antiquotations;
2017-12-04, by wenzelm
tuned;
2017-12-04, by wenzelm
tuned comments;
2017-12-04, by wenzelm
more lemmas
2017-12-04, by nipkow
misc tuning and modernization;
2017-12-03, by wenzelm
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
2017-12-03, by wenzelm
tuned;
2017-12-03, by wenzelm
misc tuning and modernization;
2017-12-03, by wenzelm
discontinued old 'def' command;
2017-12-03, by wenzelm
more simplification rules
2017-12-02, by haftmann
overhauling of primes
2017-12-02, by haftmann
cleaned up and tuned
2017-12-02, by haftmann
generalized more lemmas
2017-12-02, by haftmann
tuned output;
2017-12-01, by wenzelm
more operations;
2017-12-01, by wenzelm
removed inaccessible blobs from Document.Nodes;
2017-12-01, by wenzelm
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
2017-12-01, by wenzelm
purge hidden nodes more thoroughly: is_hidden may become true only later;
2017-12-01, by wenzelm
proper synchronized Map: this may be used on multiple threads;
2017-12-01, by wenzelm
bij_betw lemma for prime powers
2017-11-30, by eberlm
Existence of a holomorphic logarithm
2017-11-30, by eberlm
tuned;
2017-11-29, by wenzelm
clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
2017-11-29, by wenzelm
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
2017-11-28, by wenzelm
clarified description for mixed Mavericks / El Capitan system;
2017-11-27, by wenzelm
updated documentation;
2017-11-27, by wenzelm
prefer formal $POLYML_EXE;
2017-11-27, by wenzelm
clarified main sessions;
2017-11-27, by wenzelm
updated to official release of polyml-5.7.1;
2017-11-27, by wenzelm
suppress warning;
2017-11-27, by wenzelm
retain files in Pure.thy, notably $POLYML_EXE;
2017-11-27, by wenzelm
proper context (as in 'term' command);
2017-11-27, by wenzelm
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
2017-11-27, by wenzelm
more symbols;
2017-11-27, by wenzelm
prefer Input.source (via cartouche);
2017-11-27, by wenzelm
updated documentation: JVM is always 64bit;
2017-11-27, by wenzelm
more symbols;
2017-11-26, by wenzelm
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
2017-11-26, by wenzelm
macbroy2 is back, still pretending to be on Mavericks for better comparison of performance;
2017-11-25, by wenzelm
Mac OS X 10.10 Yosemite is baseline;
2017-11-25, by wenzelm
generalized more lemmas
2017-11-23, by haftmann
tuned
2017-11-23, by haftmann
tuned and generalized
2017-11-23, by haftmann
tuned
2017-11-23, by haftmann
new simp rule
2017-11-23, by haftmann
Facts about complex n-th roots
2017-11-21, by eberlm
more lemmas
2017-11-21, by nipkow
macbroy2 is inactive: system update;
2017-11-19, by wenzelm
tuned
2017-11-17, by nipkow
removed overambitious simp rules from e7e54a0b9197
2017-11-16, by haftmann
merged
2017-11-14, by Lars Hupel
instantiation char :: full_exhaustive by Andreas Lochbihler
2017-11-14, by Lars Hupel
avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries;
2017-11-14, by wenzelm
slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore (amending 2288cc39b038)
2017-11-14, by wenzelm
merged
2017-11-14, by nipkow
merged
2017-11-14, by nipkow
tuned
2017-11-14, by nipkow
removed pointless user_home: no measurable impact;
2017-11-14, by wenzelm
init Mercurial repository for the generated session files;
2017-11-13, by wenzelm
more operations;
2017-11-13, by wenzelm
tuned signature;
2017-11-13, by wenzelm
proper ssh.bash_path;
2017-11-13, by wenzelm
more operations;
2017-11-13, by wenzelm
synchronous use_theories, based on consolidated_state;
2017-11-12, by wenzelm
clarified modules;
2017-11-12, by wenzelm
optional session_base, e.g. from existing Sessions.Deps in build.scala;
2017-11-12, by wenzelm
synchronous session start (similar to isabelle.vscode.Server);
2017-11-12, by wenzelm
tuned signature (again, see 1a9e2a2bf251);
2017-11-12, by wenzelm
tuned signature;
2017-11-12, by wenzelm
simplified: eliminated pointless Thy_Document_Model;
2017-11-12, by wenzelm
theory nodes are never visible: avoid prints, which are not covered by node_consolidated;
2017-11-12, by wenzelm
load theories via PIDE document update;
2017-11-12, by wenzelm
tuned signature;
2017-11-12, by wenzelm
PIDE resources for theory files;
2017-11-12, by wenzelm
tuned;
2017-11-12, by wenzelm
tuned signature;
2017-11-12, by wenzelm
dedicated definition for coprimality
2017-11-11, by haftmann
more induct rules on nat
2017-11-11, by haftmann
avoid download of components;
2017-11-11, by wenzelm
local user_home for improved performance, but only after given changeset for stability of measurement history;
2017-11-11, by wenzelm
support alternative USER_HOME directory;
2017-11-11, by wenzelm
clarified settings environment;
2017-11-11, by wenzelm
tuned signature;
2017-11-11, by wenzelm
tuned;
2017-11-11, by wenzelm
more options for "isabelle mkroot";
2017-11-11, by wenzelm
adapted to changed ROOT syntax (see 13857f49d215);
2017-11-11, by wenzelm
converted to Isabelle/Scala;
2017-11-11, by wenzelm
replaced raw proof blocks by local lemmas
2017-11-10, by nipkow
Replaced Raw Proof Blocks by Local Lemmas
2017-11-09, by nipkow
tuned
2017-11-09, by nipkow
merged
2017-11-08, by nipkow
corrected priority
2017-11-08, by nipkow
merged
2017-11-08, by wenzelm
formal dependency on "poly" executable;
2017-11-08, by wenzelm
removed obsolete workaround: always use existing IntInf.pow;
2017-11-08, by wenzelm
strip some trailing spaces to force Pure rebuild after ce6454669360
2017-11-08, by Lars Hupel
merged
2017-11-07, by wenzelm
proper build_selection for clean_build (amending 961285f581e6): e.g. relevant for "isabelle build_doc";
2017-11-07, by wenzelm
clarified signature (again);
2017-11-07, by wenzelm
clarified exclusion: operate on completed selection, as last step;
2017-11-07, by wenzelm
tuned;
2017-11-07, by wenzelm
tuned signature;
2017-11-07, by wenzelm
clarifified selection: always wrt. build_graph structure;
2017-11-07, by wenzelm
tuned;
2017-11-07, by wenzelm
tuned signature;
2017-11-07, by wenzelm
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
2017-11-07, by blanchet
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
2017-11-07, by blanchet
added FIXMEs
2017-11-07, by blanchet
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
2017-11-07, by nipkow
backed out odd "bug fix" 671decd2e627;
2017-11-07, by wenzelm
more recent polyml-test version;
2017-11-07, by wenzelm
minimal document model for theory files;
2017-11-06, by wenzelm
tuned signature;
2017-11-06, by wenzelm
tuned signature;
2017-11-06, by wenzelm
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
2017-11-05, by wenzelm
uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");
2017-11-05, by wenzelm
updated comments;
2017-11-05, by wenzelm
updated to scala-2.12.4;
2017-11-05, by wenzelm
testing NewTestRegisterSave;
2017-11-05, by wenzelm
superseded by plain_identify;
2017-11-04, by wenzelm
tolerate odd negative times from old log files (before 1698e9ccef2d);
2017-11-04, by wenzelm
prefer main entry points of HOL;
2017-11-04, by wenzelm
tuned signature;
2017-11-04, by wenzelm
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
2017-11-04, by wenzelm
more robust sorted_entries;
2017-11-04, by wenzelm
more convenient build_log_history;
2017-11-04, by wenzelm
tuned;
2017-11-04, by wenzelm
more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
2017-11-04, by wenzelm
polyml-test version based on experimental branch NewTestRegisterSave;
2017-11-04, by wenzelm
support for libgmp on x86_64-darwin;
2017-11-03, by wenzelm
avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;
2017-11-03, by wenzelm
delegate boundary cases to existing IntInf.pow;
2017-11-03, by wenzelm
plain identify job for Isabelle + AFP, independent of any Isabelle technology;
2017-11-03, by wenzelm
tuned (non-unique example);
2017-11-03, by wenzelm
clarified situation of global theory names;
2017-11-03, by wenzelm
less global theories -- avoid confusion about special cases;
2017-11-03, by wenzelm
proper deps;
2017-11-02, by wenzelm
allow unrelated ancestor;
2017-11-02, by wenzelm
tuned;
2017-11-02, by wenzelm
support alternative ancestor session;
2017-11-02, by wenzelm
support focus_session, for much faster startup of Isabelle/jEdit;
2017-11-02, by wenzelm
more timing;
2017-11-01, by wenzelm
tuned;
2017-11-01, by wenzelm
init only once (see also c0f776b661fa);
2017-11-01, by wenzelm
proper merge (amending fb46c031c841);
2017-11-01, by wenzelm
build faster without heap images for minor imports;
2017-11-01, by wenzelm
proper order for entries from multiple profiles, notably "AFP";
2017-11-01, by wenzelm
tuned output;
2017-11-01, by wenzelm
tuned;
2017-11-01, by wenzelm
logic_selector refers to raw logic name;
2017-11-01, by wenzelm
clarified terminology;
2017-11-01, by wenzelm
tuned signature;
2017-11-01, by wenzelm
do not store bulky Session.Deps;
2017-11-01, by wenzelm
avoid duplicate invocation of expensive Sessions.deps on full_sessions;
2017-11-01, by wenzelm
added isabelle jedit options -B, -P, clarified -R;
2017-11-01, by wenzelm
no heap sharing for empty session (e.g. HOL-ODE);
2017-11-01, by wenzelm
tuned diagram;
2017-11-01, by wenzelm
clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
2017-11-01, by wenzelm
removed unused option, which is potentially expensive;
2017-10-31, by wenzelm
allow to augment session context via explicit session infos;
2017-10-31, by wenzelm
synthesize session with all required theories from other session imports;
2017-10-31, by wenzelm
clarified signature;
2017-10-31, by wenzelm
clarified signature;
2017-10-31, by wenzelm
clarified signature;
2017-10-31, by wenzelm
clarified signature;
2017-10-31, by wenzelm
clarified signature: global_theories is always required;
2017-10-31, by wenzelm
tuned;
2017-10-31, by wenzelm
tuned signature;
2017-10-31, by wenzelm
clarified modules;
2017-10-31, by wenzelm
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
2017-10-31, by wenzelm
more permissive: db could be empty after hard crash;
2017-10-31, by wenzelm
no censorship (in contrast to 2c828c830ad7);
2017-10-31, by wenzelm
A few more topological results. And made some slow proofs faster
2017-10-31, by paulson
removed ancient nat-int transfer
2017-10-31, by haftmann
added lemma
2017-10-30, by haftmann
added 'mlex_iff' lemma and simplified proof
2017-10-30, by blanchet
merged
2017-10-30, by wenzelm
recovered document from 9bfb6978eb80;
2017-10-30, by wenzelm
NEWS;
2017-10-30, by wenzelm
obsolete;
2017-10-30, by wenzelm
tuned;
2017-10-30, by wenzelm
ROOT cleanup: empty 'document_files' means there is no document;
2017-10-30, by wenzelm
eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
2017-10-30, by wenzelm
more informative timeout message, notably for build_status;
2017-10-30, by wenzelm
clarified: adapted to ML version;
2017-10-30, by wenzelm
proper order of initialization (amending 9953ae603a23);
2017-10-30, by wenzelm
More topological results overlooked last time
2017-10-30, by paulson
merged
2017-10-30, by paulson
New results in topology, mostly from HOL Light's moretop.ml
2017-10-30, by paulson
generalized some lemmas on multisets
2017-10-30, by haftmann
rule out pathologic instances
2017-10-30, by haftmann
tuned some proofs and added some lemmas
2017-10-30, by haftmann
more recent polyml-test version;
2017-10-29, by wenzelm
reduced simp_depth_limit
2017-10-29, by nipkow
generalized
2017-10-28, by immler
reduced heap hierarchy, for potentially improved performance;
2017-10-28, by wenzelm
deactivated old tests;
2017-10-28, by wenzelm
avoid slow proofs due to simp rules from 960509bfd47e;
2017-10-28, by wenzelm
some concrete commands;
2017-10-27, by wenzelm
tuned signature;
2017-10-27, by wenzelm
more formal messages;
2017-10-27, by wenzelm
tuned signature;
2017-10-27, by wenzelm
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
2017-10-27, by wenzelm
more permissive;
2017-10-27, by wenzelm
tuned;
2017-10-27, by wenzelm
separate JSON lexer;
2017-10-26, by wenzelm
clarified command language;
2017-10-26, by wenzelm
use Poly/ML 5.7.1 test version as default;
2017-10-26, by wenzelm
more explicit check;
2017-10-25, by wenzelm
more robust treatment of UTF8 in raw byte sources;
2017-10-25, by wenzelm
clarified check, assuming that load commands are plain ASCII;
2017-10-25, by wenzelm
more documentation;
2017-10-25, by wenzelm
disallow blanks, relevant for session_name / theory_name e.g. in build log files;
2017-10-25, by wenzelm
uniform system name;
2017-10-25, by wenzelm
store session sources stamp;
2017-10-24, by wenzelm
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
2017-10-24, by immler
misc tuning and modernization;
2017-10-24, by wenzelm
tuned output;
2017-10-24, by wenzelm
discontinued Linux 32bit platform support;
2017-10-23, by wenzelm
obsolete;
2017-10-23, by wenzelm
merged
2017-10-23, by wenzelm
updated to jdk-8u152, which is for x86_64 only;
2017-10-23, by wenzelm
added lemma
2017-10-23, by nipkow
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
2017-10-23, by wenzelm
tuned output;
2017-10-22, by wenzelm
updated test version;
2017-10-22, by wenzelm
merged
2017-10-22, by wenzelm
auto update;
2017-10-22, by wenzelm
more recent polyml-test version;
2017-10-22, by wenzelm
parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
2017-10-22, by wenzelm
tuned;
2017-10-22, by wenzelm
clarified signature;
2017-10-22, by wenzelm
tuned: build hg_graph only once;
2017-10-22, by wenzelm
tuned
2017-10-22, by nipkow
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
2017-10-22, by nipkow