isabelle: Graph

clarified signature: support meaningful subclasses for Build.Engine implementations;
23 months ago, by wenzelm
support alternative build engines, via system option "build_engine";
23 months ago, by wenzelm
misc tuning and clarification;
23 months ago, by wenzelm
proper test, following Platform.is_linux;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
merged
23 months ago, by paulson
Simplified some more proofs
23 months ago, by paulson
merged
23 months ago, by paulson
Replacing z powr of_int i by z powi i and adding new material from the AFP
23 months ago, by paulson
merged
23 months ago, by wenzelm
tuned: avoid redundant white space;
23 months ago, by wenzelm
clarified signature: more robust operations, without assumption about node 0;
23 months ago, by wenzelm
clarified signature: more concise operations;
23 months ago, by wenzelm
clarified modules: NUMA is managed by Build_Process;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature: move all parameters into Build_Process.Context;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
more elementary data structures, to fit better to SQL database;
23 months ago, by wenzelm
clarified signature (see also 68a7ad1385bc);
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified modules;
23 months ago, by wenzelm
merged
23 months ago, by nipkow
merge in backouts
23 months ago, by nipkow
Backed out changeset bafdc56654cf
23 months ago, by nipkow
backout rev 334015f9098e (for Main_Doc.thy only)
23 months ago, by nipkow
Backed out changeset 1fde0e4fd791
23 months ago, by nipkow
merged
23 months ago, by paulson
Simplifying more proofs
23 months ago, by paulson
merged
23 months ago, by wenzelm
proper Nodes.init (amending 9b35c1171d9a);
23 months ago, by wenzelm
unused;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
clarified signature defaults;
24 months ago, by wenzelm
clarified types: support a variety of Build_Job instances;
24 months ago, by wenzelm
clarified signature: more explicit synchronized operations;
24 months ago, by wenzelm
clarified signature: more explicit synchronized operations;
24 months ago, by wenzelm
clarified modules (again);
24 months ago, by wenzelm
clarified signature: more explicit synchronized operations;
24 months ago, by wenzelm
clarified signature: more explicit synchronized operations;
24 months ago, by wenzelm
more robust: first register job, then start job;
24 months ago, by wenzelm
clarified signature: proper scope of synchronized operation;
24 months ago, by wenzelm
proper synchronized access to mutable state, to support concurrency eventually;
24 months ago, by wenzelm
tuned signature: explicit marker for mutable global state;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
more robust;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified modules;
24 months ago, by wenzelm
merged
23 months ago, by paulson
Tidied some really messy proofs
23 months ago, by paulson
added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO
23 months ago, by desharna
Simplified a few proofs
23 months ago, by paulson
Moved up a theorem
24 months ago, by paulson
Limit properties for complex exponential
24 months ago, by paulson
More of Eberl's contributions: memomorphic functions
24 months ago, by paulson
merged
24 months ago, by paulson
New material due to Eberl on Formal Laurent Series
24 months ago, by paulson
merged
24 months ago, by paulson
A bit more tidying and some new material
24 months ago, by paulson
removed rarely used error in Sledgehammer
24 months ago, by blanchet
merged
24 months ago, by nipkow
tuned
24 months ago, by nipkow
added refute mode to Sledgehammer to find 'counterexamples'
24 months ago, by blanchet
merged
24 months ago, by nipkow
Map.map_of movement
24 months ago, by nipkow
removed Map from docu
24 months ago, by nipkow
move map_of to List
24 months ago, by nipkow
updated NEWS
24 months ago, by blanchet
careful eta-contraction in Metis to keep argument to All and Ex expanded
24 months ago, by blanchet
merged
24 months ago, by wenzelm
merged
24 months ago, by wenzelm
clarified main operations;
24 months ago, by wenzelm
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
24 months ago, by wenzelm
prefer global mutable state, in order to break up the loop eventually;
24 months ago, by wenzelm
clarified modules;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified static build_context vs. dynamic queue;
24 months ago, by wenzelm
clarified signature: make dynamic Queue from static Context;
24 months ago, by wenzelm
clarified data structure: absorb Option[Process_Result] into Process_Result, e.g. to simplify database storage;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
clarified data structure: use static info from deps, not dynamic results;
24 months ago, by wenzelm
clarified data structure: more direct access to timeout;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
misc tuning and clarification;
24 months ago, by wenzelm
clarified modules;
24 months ago, by wenzelm
tuned message: old_time not sufficiently prominent nor accurate to be printed;
24 months ago, by wenzelm
clarified signature and terminology;
24 months ago, by wenzelm
clarified signature: avoid adhoc constants;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
tuned message;
24 months ago, by wenzelm
tuned signature: more operations;
24 months ago, by wenzelm
clarified signature: more explicit types;
24 months ago, by wenzelm
clarified modules;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
merged
24 months ago, by paulson
Simplification of proofs
24 months ago, by paulson
explicit range types in abstractions
24 months ago, by stuebinm
somehow more clear terminology
24 months ago, by haftmann
tuned
24 months ago, by haftmann
Some basis results about trigonometric functions
24 months ago, by paulson
merged
24 months ago, by paulson
Even more new material from Eberl and Li
24 months ago, by paulson
merged
24 months ago, by paulson
More material for Analysis and Complex_Analysis
24 months ago, by paulson
actually executable enum_all, enum_ex for word
24 months ago, by haftmann
tuned text
24 months ago, by nipkow
Lots of new material chiefly about complex analysis
24 months ago, by paulson
merged
2023-02-07, by paulson
More new theorems from the number theory development
2023-02-07, by paulson
merged
2023-02-06, by wenzelm
proper orientation for right-associative operations;
2023-02-06, by wenzelm
tuned signature;
2023-02-06, by wenzelm
tuned signature;
2023-02-06, by wenzelm
tuned signature;
2023-02-06, by wenzelm
obsolete --- superseded by SHA1.Shasum operations;
2023-02-06, by wenzelm
clarified signature, using right-associative operation;
2023-02-06, by wenzelm
tuned whitespace;
2023-02-06, by wenzelm
tuned --- implicit split;
2023-02-06, by wenzelm
clarified signature;
2023-02-06, by wenzelm
prefer explicit shasum: more robust due to explicit file names, which often work implicitly in LaTeX;
2023-02-06, by wenzelm
tuned signature;
2023-02-06, by wenzelm
more uniform use of SHA1.Shasum;
2023-02-06, by wenzelm
proper Shasum.digest, to emulate old form from build_history database;
2023-02-06, by wenzelm
prefer explicit shasum;
2023-02-06, by wenzelm
proper symbolic dependencies, e.g. for Demo_FoilTeX;
2023-02-06, by wenzelm
prefer explicit shasum;
2023-02-06, by wenzelm
clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;
2023-02-06, by wenzelm
clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;
2023-02-06, by wenzelm
clarified signature;
2023-02-06, by wenzelm
Some more new material and some tidying of existing proofs
2023-02-06, by paulson
more diagnostic operations (see also 5c7652e9bc01);
2023-02-05, by wenzelm
more thorough consolidation: follow dependencies of forked proofs (e.g. see theories MaxPrefix vs. MaxChop in AFP/Functional-Automata);
2023-02-05, by wenzelm
clarified signature selection: SortedSet[String], which fits better to stored json and works properly on Windows (NB: document theories have an authentic session-theory name);
2023-02-05, by wenzelm
tuned;
2023-02-05, by wenzelm
clarified modules;
2023-02-05, by wenzelm
tuned signature;
2023-02-05, by wenzelm
update to polyml-5e9c8155ea96, which is more robust on arm64;
2023-02-05, by wenzelm
more robust dependencies for Pure;
2023-02-05, by wenzelm
proper compiler root for arm64;
2023-02-05, by wenzelm
clarified "isabelle build_polyml": download and build everything for current platform;
2023-02-04, by wenzelm
no view_document after build: avoid loss of focus, especially in "auto build" mode;
2023-02-03, by wenzelm
tuned message;
2023-02-03, by wenzelm
build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;
2023-02-03, by wenzelm
clarified modules;
2023-02-03, by wenzelm
maintain document_output meta data;
2023-02-03, by wenzelm
clarified modules;
2023-02-03, by wenzelm
avoid redundant SelectionChanged events;
2023-02-03, by wenzelm
more logging;
2023-02-03, by wenzelm
proper symbolic handle on component resources:
2023-02-03, by wenzelm
more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);
2023-02-03, by wenzelm
More of Manuel's material, and some changes
2023-02-02, by paulson
less verbosity by default, notably for regular "isabelle build -o document";
2023-02-01, by wenzelm
clarified message: old-style log is usually empty;
2023-02-01, by wenzelm
clarified messages, notably for session "Intro";
2023-02-01, by wenzelm
merged
2023-02-01, by wenzelm
more general program start message;
2023-02-01, by wenzelm
clarified terminology of inlined "PROGRAM START" messages;
2023-02-01, by wenzelm
isabelle update -u cite -l "";
2023-02-01, by wenzelm
less ambitious parallelism: avoid exhaustion of memory (40GB total);
2023-02-01, by wenzelm
clarified GUI;
2023-02-01, by wenzelm
clarified GUI: omit pointless search buttons, as real output is shown as markup;
2023-02-01, by wenzelm
more uniform use of Symbol.output, even in situations where its Symbol.encode is usually redundant;
2023-02-01, by wenzelm
merged
2023-02-01, by paulson
More new material thanks to Manuel
2023-02-01, by paulson
merged
2023-02-01, by nipkow
tuning
2023-02-01, by nipkow
alternate AFP tests on lrzcloud2, to fit better into one day;
2023-01-31, by wenzelm
merged
2023-01-31, by wenzelm
support document preparation from already loaded theories;
2023-01-31, by wenzelm
clarified GUI events;
2023-01-31, by wenzelm
clarified GUIs: keep related buttons together;
2023-01-31, by wenzelm
proper program name, e.g. for session "Intro";
2023-01-31, by wenzelm
clarified GUI events: reset everything on session context switch;
2023-01-31, by wenzelm
clarified GUI events: ensure fresh output when switching pages;
2023-01-31, by wenzelm
clarified GUI: avoid odd jumping pages on "Cancel";
2023-01-31, by wenzelm
clarified GUI events;
2023-01-31, by wenzelm
more accurate output: avoid output_body from last run;
2023-01-31, by wenzelm
more accurate output: avoid output_main from last run;
2023-01-31, by wenzelm
removed unused operation from 3f50b24909df;
2023-01-31, by wenzelm
clarified guard: avoid spurious auto builds;
2023-01-31, by wenzelm
automatically build document when selected theories are finished;
2023-01-31, by wenzelm
more accurate Word.capitalize: do not touch name;
2023-01-31, by wenzelm
defer build until document nodes are ready;
2023-01-31, by wenzelm
clarified signature: prefer semantic status;
2023-01-31, by wenzelm
removed obsolete parameter (see 7c23db6b857b);
2023-01-31, by wenzelm
clarified Document_Editor.Session: more explicit types, more robust operations;
2023-01-31, by wenzelm
more operations;
2023-01-30, by wenzelm
clarified operation (without change of signature!);
2023-01-30, by wenzelm
pointless
2023-01-31, by nipkow
Lots more new material thanks to Manuel Eberl
2023-01-31, by paulson
merged
2023-01-30, by paulson
Moved in a large number of highly useful library lemmas, mostly due to Manuel Eberl
2023-01-30, by paulson
observe option "show_states" in headless server (see also 951abf9db857);
2023-01-30, by wenzelm
text correction
2023-01-30, by nipkow
enable clean_components by default: it saves a lot of local disk space, notably on virtual nodes;
2023-01-29, by wenzelm
merged
2023-01-28, by wenzelm
removed somewhat pointless support for Jenkins log files: it has stopped working long ago;
2023-01-28, by wenzelm
more uniform components context for the managing "self_isabelle" and the managed "other_isabelle";
2023-01-28, by wenzelm
tuned signature;
2023-01-28, by wenzelm
more operations;
2023-01-28, by wenzelm
obsolete (see also d547173212d2);
2023-01-28, by wenzelm
clarified names to emphasize suble differences in meaning;
2023-01-28, by wenzelm
prefer high-level Other_Isabelle.bash over low-level SSH.execute;
2023-01-28, by wenzelm
unused (see 378bb7a739c3);
2023-01-28, by wenzelm
more options to manage resolved components;
2023-01-28, by wenzelm
proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);
2023-01-28, by wenzelm
tuned comments;
2023-01-28, by wenzelm
tuned;
2023-01-28, by wenzelm
clarified signature: more explicit types;
2023-01-28, by wenzelm
more operations;
2023-01-28, by wenzelm
tuned;
2023-01-28, by wenzelm
clarified signature: more robust field_scale;
2023-01-28, by wenzelm
clarified signature: more explicit types;
2023-01-28, by wenzelm
clarified signature;
2023-01-28, by wenzelm
tuned;
2023-01-27, by wenzelm
support units, e.g. java.lang.Long.MAX_VALUE is 8 EiB;
2023-01-27, by wenzelm
more explicit types;
2023-01-27, by wenzelm
prefer typed/strict operations;
2023-01-27, by wenzelm
tuned message;
2023-01-27, by wenzelm
prefer strict operation: java.io.File.length returns 0 for non-existent file;
2023-01-27, by wenzelm
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;
2023-01-27, by wenzelm
back to Scala 3.2.0 for now, since 3.2.1 causes odd crash of REPL concerning value classes (e.g. "isabelle.Time.now()");
2023-01-27, by wenzelm
Restored antiquotation.
2023-01-27, by haftmann
tuned whitespace
2023-01-26, by haftmann
merged
2023-01-27, by desharna
added lemma multpHO_plus_plus[simp]
2023-01-27, by desharna
Shortened a messy proof
2023-01-27, by paulson
Moved in some material from the AFP entry Winding_number_eval
2023-01-26, by paulson
merged
2023-01-25, by wenzelm
tuned messages: less verbosity;
2023-01-25, by wenzelm
prefer Other_Isabelle.init instead of adhoc scripts;
2023-01-25, by wenzelm
tuned message, following "isabelle components -a";
2023-01-25, by wenzelm
clean components more accurately: purge other platforms or archives;
2023-01-25, by wenzelm
more operations for SSH.System;
2023-01-25, by wenzelm
clarified signature;
2023-01-25, by wenzelm
tuned;
2023-01-25, by wenzelm
manage other Isabelle distributions via SSH;
2023-01-25, by wenzelm
more operations for SSH.System;
2023-01-25, by wenzelm