Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
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.
merged
19 months ago, by paulson
Tidied a few more proofs
19 months ago, by paulson
merged
19 months ago, by paulson
tidied a few ugly proofs
19 months ago, by paulson
let rsync re-use ssh connection via control path;
19 months ago, by wenzelm
clarified command-line;
19 months ago, by wenzelm
clarified command-line;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
proper port for Mercurial;
19 months ago, by wenzelm
clarified default: do not override port from ssh_config, which could be different from 22;
19 months ago, by wenzelm
proper Scala expression;
19 months ago, by wenzelm
clarified signature: separate unrelated modules;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
obsolete;
19 months ago, by wenzelm
obsolete;
19 months ago, by wenzelm
clarified error;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
removed remains of proxy_host management: delegated to .ssh/config;
19 months ago, by wenzelm
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
19 months ago, by wenzelm
putting together related theorems
19 months ago, by haftmann
dropped auxiliary lemma
19 months ago, by haftmann
unused;
19 months ago, by wenzelm
clarified operation: avoid perl;
19 months ago, by wenzelm
discontinued unused operations;
19 months ago, by wenzelm
clarified signature: avoid exposure of JSch types;
19 months ago, by wenzelm
clarified signature: discontinue somewhat pointless SSH.Context;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
proper path;
19 months ago, by wenzelm
Added tag Isabelle2022-RC1 for changeset 6308eaaa88f1
19 months ago, by wenzelm
clarified release packaging: naproche-20220910 lacks arm64-linux support (and crashes);
19 months ago, by wenzelm
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
19 months ago, by wenzelm
merged;
19 months ago, by wenzelm
update for release;
19 months ago, by wenzelm
more command-line options;
19 months ago, by wenzelm
less specialized euclidean relation on int
19 months ago, by haftmann
update to Isabelle2022 and Ubuntu 22.04;
19 months ago, 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;
19 months ago, by wenzelm
more operations: for testing purposes;
19 months ago, by wenzelm
provide naproche-20220910 (inactive);
19 months ago, by wenzelm
clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;
19 months ago, by wenzelm
unused;
19 months ago, by wenzelm
update for release;
19 months ago, by wenzelm
tuned: prefer Scala Regex operations;
19 months ago, by wenzelm
tuning and updates for release;
19 months ago, by wenzelm
NEWS;
19 months ago, by wenzelm
discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly);
19 months ago, by wenzelm
give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
discontinue fragile operations;
19 months ago, by wenzelm
proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);
19 months ago, by wenzelm
enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);
19 months ago, by wenzelm
updated documentation;
19 months ago, by wenzelm
support multiple sessions, with cumulative errors;
19 months ago, by wenzelm
support regex patterns on messages;
19 months ago, by wenzelm
support Pretty.unformatted, similar to ML version;
19 months ago, by wenzelm
removed odd TODO item (see 3391a493f39a);
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned output: more Pretty.item;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified failure: warning for logical error, exception for program breakdown;
19 months ago, by wenzelm
print goal instantiation for global qed (and variations);
19 months ago, by wenzelm
clarified output;
19 months ago, by wenzelm
more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);
19 months ago, by wenzelm
clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);
19 months ago, by wenzelm
updated to postgresql-42.5.0;
19 months ago, by wenzelm
tool to build Isabelle component for PostgreSQL JDBC;
19 months ago, by wenzelm
clarified goal structure with proper instantiation of main goal, to support "show_goal_inst";
19 months ago, by wenzelm
option "show_states" for more verbosity of batch-builds;
19 months ago, by wenzelm
tuned --- avoid warnings;
19 months ago, by wenzelm
proper antiquotations;
19 months ago, 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;
19 months ago, by wenzelm
proper antiquotations;
19 months ago, by wenzelm
clarified options, following e.g. "show_consts";
19 months ago, by wenzelm
proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination;
19 months ago, by wenzelm
unused (see 15758fced053);
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
show goal instantiation, notably for 'schematic_goal' command (inactive by default);
19 months ago, by wenzelm
proper umlauts;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned error message;
19 months ago, by wenzelm
merged
19 months ago, by desharna
merged
19 months ago, by desharna
moved antimono to Fun and redefined it as an abbreviation
22 months ago, by desharna
moved mono and strict_mono to Fun and redefined them as abbreviations
22 months ago, by desharna
clarified generic euclidean relation
19 months ago, by haftmann
added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number
19 months ago, by blanchet
tuned signature;
19 months ago, by wenzelm
check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned --- more robust syntax;
19 months ago, by wenzelm
tuned signature;
19 months ago, 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";
19 months ago, by wenzelm
unused (see 347ed6219dab);
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
more CONTRIBUTORS + NEWS;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
proper description;
19 months ago, by wenzelm
tuned whitespace;
19 months ago, by wenzelm
option "sort_updates" for record update simproc. Make proper record simproc definitions.
2022-03-07, by Norbert Schirmer
Merge
19 months ago, by paulson
Three new theorems about real polynomial functions
19 months ago, by paulson
tuned GUI;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
clarified GUI behaviour;
19 months ago, by wenzelm
eliminated odd Unicode blanks;
19 months ago, by wenzelm
tuned whitespace;
19 months ago, by wenzelm
eliminated DOS line endings;
19 months ago, by wenzelm
eliminated tabs, assuming tab-width=8;
19 months ago, by wenzelm
eliminated tabs, assuming tab-width=4;
19 months ago, by wenzelm
updated to current Cygwin, near 3.3.5-1;
19 months ago, by wenzelm
test macOS 12 Monterey via laramac01;
19 months ago, by wenzelm
clarified GUI update;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
more GUI functionality;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified component structure, concerning initialization order;
19 months ago, 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;
19 months ago, by wenzelm
provide cvc5-1.0.2 (inactive);
19 months ago, by wenzelm
tuned output;
19 months ago, by wenzelm
tool to build Isabelle component for cvc5;
19 months ago, by wenzelm
tuned: avoid odd stateful programming;
19 months ago, by wenzelm
more markup (for batch build);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
more NEWS;
20 months ago, by wenzelm
updated some links;
20 months ago, by wenzelm
more links, for files that formally belong to this session;
20 months ago, by wenzelm
more links;
20 months ago, by wenzelm
tuned antiquotations;
20 months ago, by wenzelm
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);
20 months ago, 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);
20 months ago, by wenzelm
proper chapter_definition to prevent odd definitions by users;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
proper order;
20 months ago, by wenzelm
tuned whitespace for presentation;
20 months ago, by wenzelm
clarified signature of Sessions.Session: chapter_defs: vs. known_chapters (in declaration order) vs. chapters (covered by visible sessions);
20 months ago, by wenzelm
clarified syntax: more uniform;
20 months ago, by wenzelm
more robust, more strict;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned output;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
clarified chapters: de-emphasize minor examples;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
produce root index based on sessions_structure.chapter_defs;
20 months ago, by wenzelm
provide chapter descriptions, based on lib/html/library_index_content.template;
20 months ago, by wenzelm
more robust: proper system_name;
20 months ago, by wenzelm
support 'chapter_definition' with description for presentation purposes;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
20 months ago, 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();
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
more robust: ensure that chapter/session/theory do not contain special notation (like "/" or "..");
20 months ago, by wenzelm
merged
20 months ago, by paulson
NEWS about Sum_of_Powers
20 months ago, by paulson
Removal of a duplicate theory, since that material and more is in the AFP: https://www.isa-afp.org/entries/Bernoulli.html
20 months ago, by paulson
NEWS;
20 months ago, by wenzelm
read full sessions_requirements, for more complete entity hyperlinks;
20 months ago, by wenzelm
more accurate management of dependencies: change of build_uuid causes output of HTML, but already existing/current HTML is not produced again;
20 months ago, by wenzelm
tuned signature: more general operations;
20 months ago, by wenzelm
tuned: avoid premature File.read;
20 months ago, by wenzelm
tuned signature: build_log db is specific to PostgreSQL;
20 months ago, by wenzelm
maintain "uuid" column in session build database, to identity the original build process uniquely;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
unused (amending 3d723062dc70);
20 months ago, by wenzelm
more readable string literals;
20 months ago, by wenzelm
avoid duplicate fact error on global_interpretation of residues
20 months ago, by haftmann
avoid looping simplification for z2
20 months ago, by haftmann
more formal meta data, within ".browser_info";
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
support for pretty-printing of JSON trees;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned: slightly more generic operations;
20 months ago, by wenzelm
remove duplicate parsing for alethe; fix skolemization;
20 months ago, by Mathias Fleury
Gauss numbers
20 months ago, by haftmann
disable laramac01 for now: system update pending;
20 months ago, by wenzelm
clarified synchronized operations: approximate file-system transactions;
20 months ago, by wenzelm
more robust concurrency: use shared Browser_Info.Context with synchronized file-system operations;
20 months ago, by wenzelm
NEWS;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned comments, following "isabelle build" usage;
20 months ago, by wenzelm
clarified names;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
proper theory_dir for links to other session;
20 months ago, by wenzelm
tuned sources and comments;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned sources and comments;
20 months ago, by wenzelm
clarified names: Browser_Info.Config vs. Browser_Info.Context;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified signature: terminology of "base" (here) vs. "root" (there);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
proper fonts_prefix (amending c14409948063): default is "" due to self-cancellation of dir;
20 months ago, by wenzelm
streamlined
20 months ago, by haftmann
simplified computation algorithm construction
20 months ago, by haftmann
merged;
20 months ago, by wenzelm
more robust GUI initialization (amending 29441f2bfe81);
20 months ago, by wenzelm
clarified signature: just one common operation;
20 months ago, by wenzelm
clarified paths and links;
20 months ago, by wenzelm
more concise output of files: just one round;
20 months ago, by wenzelm
more robust;
20 months ago, by wenzelm
proper node_dir within presentation_dir, not source file directory;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified names;
20 months ago, by wenzelm
more thorough checks of browser_info file conflicts;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
prefer strict operations with explicit errors (instead of missing HTML output);
20 months ago, by wenzelm
more thorough check, without path name artifacts (e.g. "./README");
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature: Sessions.Base_Info follows Sessions.Base;
20 months ago, by wenzelm
clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
evade clash with index.html (allow "Index.thy" even on case-insensitive file-systems);
20 months ago, by wenzelm
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
20 months ago, by wenzelm
clarified directory layout (again): mimic original directory layout, notably ISABELLE_HOME;
20 months ago, by wenzelm
more robust treatment of Document.Node.Name, following stored data;
20 months ago, by wenzelm
more robust;
20 months ago, by wenzelm
clarified directory layout: files are relative to enclosing theory;
20 months ago, by wenzelm
tuned signature: avoid duplication;
20 months ago, by wenzelm
more robust: theories could have been suppressed via option "condition";
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned messages (again, see d50c2129e73a): presentation setup could fail initially for take some time;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified signature: support for adhoc file types;
20 months ago, by wenzelm
clarified Presentation.Nodes, with explicit Nodes.Session and Nodes.Theory;
20 months ago, by wenzelm
export entity file position as well, e.g. relevant for HTML presentation with aux. files;
20 months ago, by wenzelm
proper permissive = true (amending 475fedc02737)
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
tip