isabelle: Graph

clarified error;
2022-09-12, by wenzelm
merged
2022-09-12, by wenzelm
removed remains of proxy_host management: delegated to .ssh/config;
2022-09-12, by wenzelm
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
2022-09-12, by wenzelm
putting together related theorems
2022-09-12, by haftmann
dropped auxiliary lemma
2022-09-11, by haftmann
unused;
2022-09-11, by wenzelm
clarified operation: avoid perl;
2022-09-11, by wenzelm
discontinued unused operations;
2022-09-11, by wenzelm
clarified signature: avoid exposure of JSch types;
2022-09-11, by wenzelm
clarified signature: discontinue somewhat pointless SSH.Context;
2022-09-11, by wenzelm
tuned;
2022-09-11, by wenzelm
proper path;
2022-09-11, by wenzelm
Added tag Isabelle2022-RC1 for changeset 6308eaaa88f1
2022-09-11, by wenzelm
clarified release packaging: naproche-20220910 lacks arm64-linux support (and crashes);
2022-09-10, by wenzelm
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
2022-09-10, by wenzelm
merged;
2022-09-10, by wenzelm
update for release;
2022-09-10, by wenzelm
more command-line options;
2022-09-10, by wenzelm
less specialized euclidean relation on int
2022-09-09, by haftmann
update to Isabelle2022 and Ubuntu 22.04;
2022-09-10, by wenzelm
proper comment: Phabricator remains on Ubuntu 20.04, which is still required as build environment for old Mercurial 3.9.2 with Python 2;
2022-09-10, by wenzelm
more operations: for testing purposes;
2022-09-10, by wenzelm
provide naproche-20220910 (inactive);
2022-09-10, by wenzelm
clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;
2022-09-09, by wenzelm
unused;
2022-09-09, by wenzelm
update for release;
2022-09-09, by wenzelm
tuned: prefer Scala Regex operations;
2022-09-09, by wenzelm
tuning and updates for release;
2022-09-09, by wenzelm
NEWS;
2022-09-09, by wenzelm
discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly);
2022-09-09, by wenzelm
give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;
2022-09-08, by wenzelm
merged
2022-09-08, by wenzelm
discontinue fragile operations;
2022-09-08, by wenzelm
proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);
2022-09-08, by wenzelm
enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);
2022-09-08, by wenzelm
updated documentation;
2022-09-08, by wenzelm
support multiple sessions, with cumulative errors;
2022-09-08, by wenzelm
support regex patterns on messages;
2022-09-08, by wenzelm
support Pretty.unformatted, similar to ML version;
2022-09-08, by wenzelm
removed odd TODO item (see 3391a493f39a);
2022-09-08, by wenzelm
tuned signature;
2022-09-08, by wenzelm
tuned output: more Pretty.item;
2022-09-08, by wenzelm
tuned signature;
2022-09-08, by wenzelm
clarified failure: warning for logical error, exception for program breakdown;
2022-09-08, by wenzelm
print goal instantiation for global qed (and variations);
2022-09-07, by wenzelm
clarified output;
2022-09-07, by wenzelm
more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);
2022-09-07, by wenzelm
clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);
2022-09-07, by wenzelm
updated to postgresql-42.5.0;
2022-09-07, by wenzelm
tool to build Isabelle component for PostgreSQL JDBC;
2022-09-07, by wenzelm
clarified goal structure with proper instantiation of main goal, to support "show_goal_inst";
2022-09-06, by wenzelm
option "show_states" for more verbosity of batch-builds;
2022-09-06, by wenzelm
tuned --- avoid warnings;
2022-09-06, by wenzelm
proper antiquotations;
2022-09-06, by wenzelm
inline markup for Output.state (in contrast to c94bba7906d2): make messages available via Rendering.text_messages and thus "isabelle log" (see cb0c407fbc6e), while Rendering.output_messages of Isabelle/jEdit/VSCode is unaffected;
2022-09-06, by wenzelm
proper antiquotations;
2022-09-05, by wenzelm
clarified options, following e.g. "show_consts";
2022-09-05, by wenzelm
proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination;
2022-09-05, by wenzelm
unused (see 15758fced053);
2022-09-05, by wenzelm
clarified modules;
2022-09-05, by wenzelm
show goal instantiation, notably for 'schematic_goal' command (inactive by default);
2022-09-05, by wenzelm
proper umlauts;
2022-09-05, by wenzelm
tuned signature;
2022-09-05, by wenzelm
tuned signature;
2022-09-05, by wenzelm
tuned;
2022-09-05, by wenzelm
tuned;
2022-09-05, by wenzelm
tuned error message;
2022-09-05, by wenzelm
merged
2022-09-07, by desharna
merged
2022-09-02, by desharna
moved antimono to Fun and redefined it as an abbreviation
2022-06-25, by desharna
moved mono and strict_mono to Fun and redefined them as abbreviations
2022-06-25, by desharna
clarified generic euclidean relation
2022-09-05, by haftmann
added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number
2022-09-05, by blanchet
tuned signature;
2022-09-03, by wenzelm
check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";
2022-09-03, by wenzelm
tuned signature;
2022-09-03, by wenzelm
tuned --- more robust syntax;
2022-09-03, by wenzelm
tuned signature;
2022-09-03, by wenzelm
back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error "Cannot update finished theory CTT.Elimination";
2022-09-03, by wenzelm
unused (see 347ed6219dab);
2022-09-03, by wenzelm
tuned signature;
2022-09-03, by wenzelm
more CONTRIBUTORS + NEWS;
2022-09-02, by wenzelm
tuned;
2022-09-02, by wenzelm
proper description;
2022-09-02, by wenzelm
tuned whitespace;
2022-09-02, by wenzelm
option "sort_updates" for record update simproc. Make proper record simproc definitions.
2022-03-07, by Norbert Schirmer
Merge
2022-09-01, by paulson
Three new theorems about real polynomial functions
2022-09-01, by paulson
tuned GUI;
2022-09-01, by wenzelm
tuned;
2022-09-01, by wenzelm
clarified GUI behaviour;
2022-09-01, by wenzelm
eliminated odd Unicode blanks;
2022-08-31, by wenzelm
tuned whitespace;
2022-08-31, by wenzelm
eliminated DOS line endings;
2022-08-31, by wenzelm
eliminated tabs, assuming tab-width=8;
2022-08-31, by wenzelm
eliminated tabs, assuming tab-width=4;
2022-08-31, by wenzelm
updated to current Cygwin, near 3.3.5-1;
2022-08-31, by wenzelm
test macOS 12 Monterey via laramac01;
2022-08-31, by wenzelm
clarified GUI update;
2022-08-31, by wenzelm
clarified signature;
2022-08-31, by wenzelm
tuned signature;
2022-08-31, by wenzelm
more GUI functionality;
2022-08-31, by wenzelm
clarified signature;
2022-08-31, by wenzelm
clarified component structure, concerning initialization order;
2022-08-30, by wenzelm
update VSCodium 1.65.2 ~> 1.70.1, Electron 13.5.2 ~> 18.3.5, Node.js v14.16.0 ~> v16.13.2;
2022-08-29, by wenzelm
provide cvc5-1.0.2 (inactive);
2022-08-29, by wenzelm
tuned output;
2022-08-29, by wenzelm
tool to build Isabelle component for cvc5;
2022-08-29, by wenzelm
tuned: avoid odd stateful programming;
2022-08-29, by wenzelm
more markup (for batch build);
2022-08-28, by wenzelm
tuned;
2022-08-28, by wenzelm
tuned;
2022-08-28, by wenzelm
tuned;
2022-08-28, by wenzelm
more NEWS;
2022-08-28, by wenzelm
updated some links;
2022-08-28, by wenzelm
more links, for files that formally belong to this session;
2022-08-28, by wenzelm
more links;
2022-08-28, by wenzelm
tuned antiquotations;
2022-08-28, by wenzelm
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);
2022-08-27, by wenzelm
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
2022-08-27, by wenzelm
proper chapter_definition to prevent odd definitions by users;
2022-08-27, by wenzelm
tuned;
2022-08-27, by wenzelm
tuned signature;
2022-08-27, by wenzelm
proper order;
2022-08-27, by wenzelm
tuned whitespace for presentation;
2022-08-27, by wenzelm
clarified signature of Sessions.Session: chapter_defs: vs. known_chapters (in declaration order) vs. chapters (covered by visible sessions);
2022-08-27, by wenzelm
clarified syntax: more uniform;
2022-08-27, by wenzelm
more robust, more strict;
2022-08-27, by wenzelm
tuned signature;
2022-08-27, by wenzelm
tuned;
2022-08-27, by wenzelm
tuned output;
2022-08-26, by wenzelm
merged
2022-08-26, by wenzelm
clarified chapters: de-emphasize minor examples;
2022-08-26, by wenzelm
tuned signature;
2022-08-26, by wenzelm
clarified signature;
2022-08-26, by wenzelm
produce root index based on sessions_structure.chapter_defs;
2022-08-26, by wenzelm
provide chapter descriptions, based on lib/html/library_index_content.template;
2022-08-26, by wenzelm
more robust: proper system_name;
2022-08-26, by wenzelm
support 'chapter_definition' with description for presentation purposes;
2022-08-26, by wenzelm
tuned whitespace;
2022-08-26, by wenzelm
tuned signature;
2022-08-26, by wenzelm
removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
2022-08-26, by wenzelm
more aggressive clean_directory(session_dir), while rm_tree is guarded by check_directory, i.e. it is presumably "owned" by Browser_Info.build_session();
2022-08-26, by wenzelm
clarified signature;
2022-08-26, by wenzelm
tuned signature;
2022-08-26, by wenzelm
clarified signature;
2022-08-26, by wenzelm
tuned whitespace;
2022-08-26, by wenzelm
more robust: ensure that chapter/session/theory do not contain special notation (like "/" or "..");
2022-08-26, by wenzelm
merged
2022-08-26, by paulson
NEWS about Sum_of_Powers
2022-08-25, by paulson
Removal of a duplicate theory, since that material and more is in the AFP: https://www.isa-afp.org/entries/Bernoulli.html
2022-08-25, by paulson
NEWS;
2022-08-25, by wenzelm
read full sessions_requirements, for more complete entity hyperlinks;
2022-08-25, by wenzelm
more accurate management of dependencies: change of build_uuid causes output of HTML, but already existing/current HTML is not produced again;
2022-08-25, by wenzelm
tuned signature: more general operations;
2022-08-25, by wenzelm
tuned: avoid premature File.read;
2022-08-25, by wenzelm
tuned signature: build_log db is specific to PostgreSQL;
2022-08-25, by wenzelm
maintain "uuid" column in session build database, to identity the original build process uniquely;
2022-08-25, by wenzelm
tuned signature;
2022-08-25, by wenzelm
unused (amending 3d723062dc70);
2022-08-25, by wenzelm
more readable string literals;
2022-08-25, by wenzelm
avoid duplicate fact error on global_interpretation of residues
2022-08-24, by haftmann
avoid looping simplification for z2
2022-08-24, by haftmann
more formal meta data, within ".browser_info";
2022-08-22, by wenzelm
tuned signature;
2022-08-22, by wenzelm
support for pretty-printing of JSON trees;
2022-08-22, by wenzelm
tuned signature;
2022-08-22, by wenzelm
tuned: slightly more generic operations;
2022-08-22, by wenzelm
remove duplicate parsing for alethe; fix skolemization;
2022-08-22, by Mathias Fleury
Gauss numbers
2022-08-21, by haftmann
disable laramac01 for now: system update pending;
2022-08-21, by wenzelm
clarified synchronized operations: approximate file-system transactions;
2022-08-21, by wenzelm
more robust concurrency: use shared Browser_Info.Context with synchronized file-system operations;
2022-08-21, by wenzelm
NEWS;
2022-08-21, by wenzelm
tuned;
2022-08-21, by wenzelm
tuned comments, following "isabelle build" usage;
2022-08-21, by wenzelm
clarified names;
2022-08-21, by wenzelm
clarified modules;
2022-08-21, by wenzelm
proper theory_dir for links to other session;
2022-08-21, by wenzelm
tuned sources and comments;
2022-08-21, by wenzelm
clarified signature;
2022-08-21, by wenzelm
tuned sources and comments;
2022-08-21, by wenzelm
clarified names: Browser_Info.Config vs. Browser_Info.Context;
2022-08-21, by wenzelm
clarified modules;
2022-08-21, by wenzelm
clarified signature: terminology of "base" (here) vs. "root" (there);
2022-08-21, by wenzelm
tuned;
2022-08-21, by wenzelm
proper fonts_prefix (amending c14409948063): default is "" due to self-cancellation of dir;
2022-08-21, by wenzelm
streamlined
2022-08-21, by haftmann
simplified computation algorithm construction
2022-08-21, by haftmann
merged;
2022-08-20, by wenzelm
more robust GUI initialization (amending 29441f2bfe81);
2022-08-20, by wenzelm
clarified signature: just one common operation;
2022-08-20, by wenzelm
clarified paths and links;
2022-08-20, by wenzelm
more concise output of files: just one round;
2022-08-20, by wenzelm
more robust;
2022-08-20, by wenzelm
proper node_dir within presentation_dir, not source file directory;
2022-08-20, by wenzelm
clarified modules;
2022-08-20, by wenzelm
clarified names;
2022-08-20, by wenzelm
more thorough checks of browser_info file conflicts;
2022-08-20, by wenzelm
tuned;
2022-08-20, by wenzelm
prefer strict operations with explicit errors (instead of missing HTML output);
2022-08-20, by wenzelm
more thorough check, without path name artifacts (e.g. "./README");
2022-08-20, by wenzelm
tuned signature;
2022-08-20, by wenzelm
clarified signature: Sessions.Base_Info follows Sessions.Base;
2022-08-20, by wenzelm
clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
2022-08-20, by wenzelm
tuned;
2022-08-20, by wenzelm
tuned whitespace;
2022-08-20, by wenzelm
evade clash with index.html (allow "Index.thy" even on case-insensitive file-systems);
2022-08-20, by wenzelm
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
2022-08-19, by wenzelm
clarified directory layout (again): mimic original directory layout, notably ISABELLE_HOME;
2022-08-19, by wenzelm
more robust treatment of Document.Node.Name, following stored data;
2022-08-19, by wenzelm
more robust;
2022-08-19, by wenzelm
clarified directory layout: files are relative to enclosing theory;
2022-08-19, by wenzelm
tuned signature: avoid duplication;
2022-08-19, by wenzelm
more robust: theories could have been suppressed via option "condition";
2022-08-19, by wenzelm
tuned signature;
2022-08-19, by wenzelm
tuned messages (again, see d50c2129e73a): presentation setup could fail initially for take some time;
2022-08-19, by wenzelm
clarified modules;
2022-08-19, by wenzelm
clarified signature: support for adhoc file types;
2022-08-19, by wenzelm
clarified Presentation.Nodes, with explicit Nodes.Session and Nodes.Theory;
2022-08-19, by wenzelm
export entity file position as well, e.g. relevant for HTML presentation with aux. files;
2022-08-19, by wenzelm
proper permissive = true (amending 475fedc02737)
2022-08-19, by wenzelm
tuned signature;
2022-08-19, by wenzelm
clarified signature;
2022-08-19, by wenzelm
clarified signature;
2022-08-18, by wenzelm
more robust directory structure: always relative to session_dir;
2022-08-18, by wenzelm
discontinued slightly odd integrity check (from af2d0e07493b): requires a different approach;
2022-08-18, by wenzelm
clarified signature;
2022-08-18, by wenzelm
misc tuning and clarification;
2022-08-18, by wenzelm
unused;
2022-08-18, by wenzelm
tuned signature;
2022-08-17, by wenzelm
tuned signature;
2022-08-17, by wenzelm
tuned signature;
2022-08-17, by wenzelm
clarified modules;
2022-08-17, by wenzelm
clarified modules;
2022-08-17, by wenzelm
unused;
2022-08-17, by wenzelm
tuned signature;
2022-08-17, by wenzelm
clarified signature: replaced Sessions.Deps by Sessions.Structure from HTML_Context;
2022-08-17, by wenzelm
tuned;
2022-08-17, by wenzelm
clarified signature: avoid constants from Sessions.Structure within Session.Base;
2022-08-17, by wenzelm
clarified signature: avoid object-oriented HTML_Context;
2022-08-17, by wenzelm
tuned type signature
2022-08-19, by haftmann
tuned type signature
2022-08-19, by haftmann
streamlined theorems
2022-08-19, by haftmann
more thorough split rules for div and mod on numerals, tuned split rules setup
2022-08-19, by haftmann
streamlined simpset building, avoiding duplicated rewrite rules
2022-08-19, by haftmann
consolidated attribute name
2022-08-19, by haftmann
streamlined theorems
2022-08-19, by haftmann
streamlined theorems and sections
2022-08-19, by haftmann
streamlined primitive definitions for integer division
2022-08-17, by haftmann
reintroduced SPASS to the mix
2022-08-18, by blanchet
tweaked generation of Isar proofs
2022-08-17, by blanchet
tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s
2022-08-17, by blanchet
tuned comments;
2022-08-17, by wenzelm
updated to sumatra_pdf-3.4.6;
2022-08-17, by wenzelm
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
2022-08-17, by wenzelm
revived 'try0' and 'smart' Isar proofs in Sledgehammer
2022-08-16, by blanchet
Cleanup of NonstandardAnalysis
2022-08-16, by paulson
A bit of cleaning up
2022-08-15, by paulson
The same, without adding a new simprule
2022-08-15, by paulson
moved some material from Sum_of_Powers
2022-08-14, by paulson
merged
2022-08-14, by wenzelm
clarified signature;
2022-08-14, by wenzelm
clarified theory_names with exported content;
2022-08-14, by wenzelm
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
2022-08-14, by wenzelm
proper treatment of empty lines (amending 08f89f0e8a62);
2022-08-14, by wenzelm
clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);
2022-08-14, by wenzelm
merged
2022-08-14, by paulson
The right way to formulate card_UNION, plus the old version for compatibility
2022-08-13, by paulson
tuned comments;
2022-08-13, by wenzelm
tuned signature;
2022-08-13, by wenzelm
clarified signature;
2022-08-13, by wenzelm
clarified signature;
2022-08-13, by wenzelm
clarified signature;
2022-08-13, by wenzelm
unused;
2022-08-13, by wenzelm
clarified modules;
2022-08-13, by wenzelm
clarified signature;
2022-08-13, by wenzelm
clarified signature: more explicit types;
2022-08-13, by wenzelm
clarified signature --- avoid dependent types;
2022-08-13, by wenzelm
tuned whitespace;
2022-08-13, by wenzelm
clarified signature: avoid public representation;
2022-08-13, by wenzelm
tuned signature;
2022-08-13, by wenzelm
clarified signature;
2022-08-13, by wenzelm
unused;
2022-08-13, by wenzelm
more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
2022-08-13, by wenzelm
clarified signature: more explicit types;
2022-08-13, by wenzelm
tuned whitespace;
2022-08-13, by wenzelm
tuned, following 298707451ec2;
2022-08-13, by wenzelm
unused;
2022-08-13, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-13, by wenzelm
clarified signature: more explicit types;
2022-08-13, by wenzelm
tuned whitespace;
2022-08-13, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-13, by wenzelm
merged
2022-08-12, by wenzelm
more GUI elements;
2022-08-12, by wenzelm
clarified signature;
2022-08-12, by wenzelm
tuned;
2022-08-12, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-12, by wenzelm
clarified signature --- more operations;
2022-08-12, by wenzelm
clarified signature --- simplified types;
2022-08-12, by wenzelm
tuned signature;
2022-08-12, by wenzelm
proper toString for Content_XML, which is not covered by trait Content;
2022-08-12, by wenzelm
clarified output;
2022-08-12, by wenzelm
clarified signature: support different document_session, e.g. within running PIDE session;
2022-08-12, by wenzelm
unused (despite cf52379c0776);
2022-08-12, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-12, by wenzelm
unused (see 696819fe2424);
2022-08-12, by wenzelm
clarified signature;
2022-08-12, by wenzelm
basic setup for document build panel;
2022-08-12, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-12, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-12, by wenzelm
tuned;
2022-08-12, by wenzelm
clarified signature;
2022-08-12, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-12, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-12, by wenzelm
tuned signature;
2022-08-12, by wenzelm
tuned signature;
2022-08-12, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
2022-08-12, by wenzelm
added support for cvc5 (whose interface is almost identical to CVC4)
2022-08-12, by blanchet
removing the [simp] attribute breaks too many AFP entries severely
2022-08-11, by nipkow
nlists is picked up automatically but conflicts with the RBT setup
2022-08-11, by nipkow
new lemma
2022-08-11, by nipkow
merged
2022-08-11, by nipkow
New theory of fixed length lists
2022-08-10, by nipkow
Further streamlining of quick-and-dirty evaluation.
2022-08-10, by haftmann
more correct approximation (contributed by Achim Brucker)
2022-07-25, by Achim D. Brucker
Added tag Isabelle2022-RC0 for changeset b42e20adaeed
2022-08-08, by wenzelm
proper Java/Scala compiler classpath for standalone application (see also make_isabelle_app() in Pure/Admin/build_release.scala);
2022-08-08, by wenzelm
clarified message;
2022-08-08, by wenzelm
provide naproche-20220808 (inactive);
2022-08-08, by wenzelm
more robust data representation: notably for Store.read_session_timing with database_server;
2022-08-08, by wenzelm
tuned message;
2022-08-07, by wenzelm
afford default cache policy, despite 6a29709906c6;
2022-08-07, by wenzelm
tuned signature;
2022-08-07, by wenzelm
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
2022-08-07, by wenzelm
tuned;
2022-08-07, by wenzelm
tuned signature;
2022-08-07, by wenzelm
clarified signature;
2022-08-07, by wenzelm
clarified modules;
2022-08-07, by wenzelm
merged
2022-08-06, by wenzelm
tuned;
2022-08-06, by wenzelm
clarified message;
2022-08-06, by wenzelm
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
2022-08-06, by wenzelm
clarified signature: prefer Export.Context;
2022-08-06, by wenzelm
clarified signature: find session_database within Session_Context.db_hierarchy;
2022-08-06, by wenzelm
clarified signature: prefer Export.Session_Context;
2022-08-06, by wenzelm
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
2022-08-06, by wenzelm
clarified signature;
2022-08-06, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
2022-08-06, by wenzelm
clarified signature: more robust treatment of server;
2022-08-06, by wenzelm
discontinued Export.Provider in favour of Export.Context and its derivatives;
2022-08-05, by wenzelm
clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;
2022-08-05, by wenzelm
tuned signature: more operations;
2022-08-05, by wenzelm
misc tuning and clarification;
2022-08-05, by wenzelm
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
2022-08-05, by wenzelm
clarified database query: refer to semantic theories;
2022-08-05, by wenzelm
clarified signature: more operations;
2022-08-05, by wenzelm
clarified signature: persistent theory_names in lexical order;
2022-08-05, by wenzelm
proper session_databases for database_server: need to follow precise session_hierarchy;
2022-08-05, by wenzelm
redundant;
2022-08-05, by wenzelm
clarified signature: more robust close operation;
2022-08-05, by wenzelm
more uniform exports: proper encoding of empty parents for Pure;
2022-08-05, by wenzelm
clarified signature: more uniform treatment of empty exports;
2022-08-05, by wenzelm
clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions;
2022-08-05, by wenzelm
more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
2022-08-05, by wenzelm
clarified context for retrieval: more explicit types, with optional close() operation;
2022-08-04, by wenzelm
tuned;
2022-08-04, by wenzelm
unused;
2022-08-04, by wenzelm
retrieve information about used files;
2022-08-04, by wenzelm
tuned signature -- more robust;
2022-08-04, by wenzelm
tuned signature;
2022-08-04, by wenzelm
clarified signature: Export.Provider knows its (accidental) theory_names;
2022-08-04, by wenzelm
clarified signature;
2022-08-04, by wenzelm
tuned, following hints by IntelliJ IDEA;
2022-08-04, by wenzelm
clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
2022-08-04, by wenzelm
tuned signature;
2022-08-04, by wenzelm
clarified signature;
2022-08-03, by wenzelm
clarified signature;
2022-08-03, by wenzelm
clarified signature;
2022-08-03, by wenzelm
avoid multiple load_commands;
2022-08-03, by wenzelm
avoid redundant dependencies.load_commands with potential errors (amending ea4f86914cb2);
2022-08-03, by wenzelm
tuned signature -- avoid redundant arguments;
2022-08-03, by wenzelm
tuned -- following hints by IntelliJ IDEA;
2022-08-03, by wenzelm
tuned signature;
2022-08-03, by wenzelm
tuned comments;
2022-08-03, by wenzelm
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
2022-08-03, by wenzelm
tuned signature;
2022-08-02, by wenzelm
clarified signature;
2022-08-02, by wenzelm
clarified signature: avoid repeated db_context.input_database;
2022-08-02, by wenzelm
clarified signature: more robust;
2022-08-02, by wenzelm
removed somewhat pointless operations (see a6c69599ab99);
2022-08-02, by wenzelm
clarified signature;
2022-07-30, by wenzelm
tuned;
2022-07-30, by wenzelm
tuned;
2022-07-30, by wenzelm
clarified signature;
2022-07-30, by wenzelm
clarified names;
2022-07-30, by wenzelm
clarified signature;
2022-07-30, by wenzelm
clarified names;
2022-07-30, by wenzelm
clarified signature;
2022-07-30, by wenzelm
clarified signature: more explicit types;
2022-07-30, by wenzelm
unused (see 0d30ea76756c);
2022-07-29, by wenzelm
tuned;
2022-07-29, by wenzelm
clarified signature;
2022-07-29, by wenzelm
tuned;
2022-07-29, by wenzelm
unused (see 3064e165c660);
2022-07-29, by wenzelm
merge
2022-08-02, by blanchet
changed the order of Zipperposition slices in Sledgehammer
2022-08-02, by blanchet
merged
2022-08-02, by paulson
The wellordering instantiation for length-ordered lists
2022-08-02, by paulson
show sum_list defn
2022-08-02, by nipkow
prettified def
2022-07-29, by nipkow
More lemmas.
2022-07-28, by haftmann
Some more proofs.
2022-07-28, by haftmann
a few new theorems
2022-07-28, by paulson
tuned;
2022-07-27, by wenzelm
clarified while-loops;
2022-07-27, by wenzelm
updated to postgresql-42.4.0;
2022-07-27, by wenzelm
updated to flatlaf-2.4;
2022-07-27, by wenzelm
updated to pdfjs-2.14.305;
2022-07-27, by wenzelm
more robust: retain Classpath value;
2022-07-27, by wenzelm
tuned;
2022-07-27, by wenzelm
mor robust;
2022-07-27, by wenzelm
clarified modules;
2022-07-27, by wenzelm
clarified signature;
2022-07-27, by wenzelm
update documentation, following 21c1f82e7f5d;
2022-07-26, by wenzelm
proper classpath for Scala compiler invocation (amending 14e22b525b13);
2022-07-26, by wenzelm
merged
2022-07-26, by wenzelm
support for dynamic classpath from exports;
2022-07-26, by wenzelm
clarified signature;
2022-07-25, by wenzelm
tuned signature;
2022-07-25, by wenzelm
Avoid shadowing original List._ namespace.
2022-07-25, by haftmann
replaced complicated lemma by a simpler one
2022-07-25, by nipkow
clarified signature;
2022-07-23, by wenzelm
clarified modules;
2022-07-23, by wenzelm
merged
2022-07-22, by wenzelm
more documentation;
2022-07-22, by wenzelm
tuned;
2022-07-22, by wenzelm
removed obsolete commands;
2022-07-22, by wenzelm
command 'scala_build_generated_files' with proper management of source dependencies;
2022-07-22, by wenzelm
clarified signature;
2022-07-21, by wenzelm
tuned messages;
2022-07-21, by wenzelm
support more file types;
2022-07-21, by wenzelm
support for Java language;
2022-07-21, by wenzelm
clarified signature;
2022-07-12, by wenzelm
clarified signature;
2022-07-12, by wenzelm
support for classpath artifacts within session structure:
2022-07-12, by wenzelm
clarified names;
2022-07-12, by wenzelm
clarified signature;
2022-07-12, by wenzelm
clarified signature;
2022-07-11, by wenzelm
clarified signature;
2022-07-11, by wenzelm
clarified signature;
2022-07-11, by wenzelm
unused;
2022-07-11, by wenzelm
clarified signature;
2022-07-11, by wenzelm
tuned signature: more explicit types;
2022-07-11, by wenzelm
fix document build error
2022-07-22, by Lukas Stevens
tuned (some HOL lints, by Yecine Megdiche);
2022-07-22, by Fabian Huch
moved lemma fromm AFP
2022-07-15, by nipkow
tuned names
2022-07-15, by nipkow
refined code equations for characters
2022-07-12, by haftmann
prefer non-JNI SAT solvers by default in Nitpick
2022-07-11, by blanchet
milder Sledgehammer messages
2022-07-11, by blanchet
moved lemmas from AFP
2022-07-11, by nipkow
refined code equations for characters
2022-07-09, by haftmann
tuned comments;
2022-07-08, by wenzelm
support for Isabelle/Scala/Java modules in Isabelle/ML;
2022-07-08, by wenzelm
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
2022-07-08, by wenzelm
clarified signature: read_theory_exports is already ordered;
2022-07-08, by wenzelm
clarified signature;
2022-07-07, by wenzelm
tuned;
2022-07-07, by wenzelm
sketch for word-specific lsb and msb
2022-07-06, by haftmann
switch to Scala 3;
2022-07-05, by wenzelm
minor performance tuning: avoid redundant BigInt construction;
2022-07-06, by wenzelm
added lemmas total_on_trancl and totalp_on_tranclp
2022-07-05, by desharna
Move code lemmas for symbolic computation of bit operations on int to distribution.
2022-07-04, by haftmann
fixed diverging simproc cont_intro
2022-07-05, by desharna
corrections and adjustions for Scala 3
2022-07-04, by haftmann
more complete set of code equations
2022-07-04, by haftmann
officical abstract characters for code generation
2022-07-04, by haftmann
provide components for scala3 (still inactive);
2022-07-01, by wenzelm