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