Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+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.
tuned signature;
16 months ago, by wenzelm
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
16 months ago, by wenzelm
update URL;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature: more explicit types;
16 months ago, by wenzelm
merged
16 months ago, by desharna
merged
16 months ago, by desharna
used transp_on in assumptions of lemmas Multiset.bex_(least|greatest)_element
16 months ago, by desharna
added lemma trans_on_lex_prod[simp]
16 months ago, by desharna
strengthened and renamed lemma trans_converse and added lemma transp_on_conversep
16 months ago, by desharna
strengthened and renamed trans_reflclI
16 months ago, by desharna
strengthened and renamed transp_reflclp
16 months ago, by desharna
strengthened and renamed lemmas preorder.transp_(ge|gr|le|less)
16 months ago, by desharna
added lemmas trans_on_subset and transp_on_subset
16 months ago, by desharna
added lemmas trans_onD and transp_onD
16 months ago, by desharna
added lemmas trans_onI and transp_onI
16 months ago, by desharna
added lemma transp_on_trans_on_eq[pred_set_conv]
16 months ago, by desharna
fixed code-generation failure
16 months ago, by desharna
added predicates trans_on and transp_on and redefined trans and transp to be abbreviations
16 months ago, by desharna
only show sessions with document setup;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
proper node name instead of not base tex_name (amending 2fd0c33fe440);
16 months ago, by wenzelm
proper migrate_name between different kinds of Resources, notably for Windows;
16 months ago, by wenzelm
merged
16 months ago, by desharna
added lemmas irrefl_on_if_asym_on[simp] and irreflp_on_if_asymp_on[simp]
16 months ago, by desharna
proper PIDE session background for interactive document context;
16 months ago, by wenzelm
NEWS;
16 months ago, by wenzelm
more accurate error messages;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
actually build document;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned comments;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified GUI;
16 months ago, by wenzelm
more thorough GUI updates, notably for multiple Document dockables;
16 months ago, by wenzelm
Additional new material about infinite products, etc.
16 months ago, by paulson
merged
16 months ago, by paulson
First round of moving material from the number theory development
16 months ago, by paulson
merged
16 months ago, by wenzelm
more GUI operations;
16 months ago, by wenzelm
proper handling of state updates;
16 months ago, by wenzelm
clarified process management;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified state document nodes for Theories_Status / Document_Dockable;
16 months ago, by wenzelm
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
clarified module initialization;
16 months ago, by wenzelm
tuned signature, following Document_Dockable;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified GUI;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
proper thread context;
16 months ago, by wenzelm
more informative errors, including optional Exn.trace;
16 months ago, by wenzelm
clarified state change: presumably more robust;
16 months ago, by wenzelm
proper state change, e.g. on open/close of "Document" panel;
16 months ago, by wenzelm
clarified module initialization;
16 months ago, by wenzelm
clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
added lifting_forget as suggested by Peter Lammich
16 months ago, by blanchet
merged
16 months ago, by desharna
added lemma refl_lex_prod[simp]
16 months ago, by desharna
added lemmas reflI and reflD
16 months ago, by desharna
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
16 months ago, by desharna
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
16 months ago, by desharna
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
16 months ago, by desharna
strengthened and renamed lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
16 months ago, by desharna
strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep
16 months ago, by desharna
added lemmas asym_on_converse[simp] and asymp_on_conversep[simp]
16 months ago, by desharna
strengthened and renamed lemma sym_converse and added lemma symp_on_conversep
16 months ago, by desharna
strengthened and renamed lemmas antisymp_less and antisymp_greater
16 months ago, by desharna
strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on
16 months ago, by desharna
tuned naming
16 months ago, by desharna
added lemma asymp_on_asym_on_eq[pred_set_conv]
16 months ago, by desharna
strengthened and renamed asymp_less and asymp_greater
16 months ago, by desharna
added lemmas asym_on_subset and asymp_on_subset
16 months ago, by desharna
added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD
16 months ago, by desharna
added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations
16 months ago, by desharna
clarified state and process;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
merged
16 months ago, by desharna
strengthened and renamed symp_symclp
16 months ago, by desharna
merged
16 months ago, by nipkow
Tuned text
16 months ago, by nipkow
clarified signature: avoid confusion due to redundant standard_path, which is already used here (but not elsewhere);
16 months ago, by wenzelm
clarified signature: avoid case class with redefined equality;
16 months ago, by wenzelm
discontinued somewhat pointless dependency: avoid illusion of extra accuracy (see also 09fb749d1a1e and 0f750a6dc754);
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
unused;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned output;
16 months ago, by wenzelm
prefer SML here
16 months ago, by haftmann
Typo.
16 months ago, by haftmann
merged
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified names;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature (see also 8342cba8eae8);
16 months ago, by wenzelm
tuned names: avoid overlap with instances of class Resources;
16 months ago, by wenzelm
merged
16 months ago, by nipkow
file with partial function docu
16 months ago, by nipkow
Added section about code generation for partial functions
16 months ago, by nipkow
added lemmas sym_on_subset and symp_on_subset
16 months ago, by desharna
added lemmas sym_onD and symp_onD
16 months ago, by desharna
added lemmas sym_onI and symp_onI
16 months ago, by desharna
added lemma symp_on_sym_on_eq[pred_set_conv]
16 months ago, by desharna
added predicates sym_on and symp_on and redefined sym and symp to be abbreviations
16 months ago, by desharna
added lemmas IMGU_subst_domain_subset and IMGU_range_vars_subset
16 months ago, by desharna
added lemmas antisym_on_subset and antisymp_on_subset
16 months ago, by desharna
strengthened antisymp_le and antisymp_ge
16 months ago, by desharna
added lemmas antisym_onD and antisymp_onD
16 months ago, by desharna
added lemmas antisym_onI and antisymp_onI
16 months ago, by desharna
added lemma antisymp_reflcp
16 months ago, by desharna
added antisymp_on_antisym_on_eq[pred_set_conv]
16 months ago, by desharna
added predicates antisym_on and antisymp_on and redefined antisym and antisymp to be abbreviations
16 months ago, by desharna
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified order: accumulate strictly from left to right;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified signature: more types and operations;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
proper file extension for Isabelle_System.extract;
16 months ago, by wenzelm
tuned implementation;
16 months ago, by wenzelm
more uniform use of make_directory;
16 months ago, by wenzelm
tuned message;
16 months ago, by wenzelm
tuned: less redundant implementation;
16 months ago, by wenzelm
clarified signature: copy directory content more directly;
16 months ago, by wenzelm
more robust;
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
clarified signature: more general operations;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
merged
16 months ago, by desharna
Strengthened multiset lemmas w.r.t. irrefl and irreflp
16 months ago, by desharna
clarified signature: proper scopes and types;
16 months ago, by wenzelm
maintain global state of document editor views, notably for is_active operation;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
clarified signature: more robust;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
more specific GUI for document nodes;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
clarified signature: just one level of arguments to avoid type-inference problems;
16 months ago, by wenzelm
tuned signature: more operations;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
stated goals of some lemmas explicitely to prevent silent changes
16 months ago, by desharna
rewrite proofs using to_pred attribute on existing lemmas
16 months ago, by desharna
clarified signature: less redundancy;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
potentially more robust delay_load action: avoid loosing events due to guards;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
more uniform tooltip for plugin options dialog;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
more uniform session selectors, with persistent options;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
NEWS
16 months ago, by desharna
merged
16 months ago, by desharna
added lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
17 months ago, by desharna
added lemma totalp_on_converse[simp]
17 months ago, by desharna
added lemmas irrefl_on_converse[simp] and irreflp_on_converse[simp]
17 months ago, by desharna
added type annotations and tuned formatting
17 months ago, by desharna
strengthened and renamed irreflp_greater[simp] and irreflp_less[simp]
17 months ago, by desharna
merged
16 months ago, by wenzelm
tuned GUI behaviour;
16 months ago, by wenzelm
more GUI elements;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
clarified process: implicit load() when finished;
16 months ago, by wenzelm
more robust, notably initial update();
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned messages: implement "verbose = false", but there is no theory output anyway;
16 months ago, by wenzelm
merged
16 months ago, by desharna
added lemmas irrefl_on_subset and irreflp_on_subset
17 months ago, by desharna
introduced predicates irrefl_on and irreflp_on, and redefined irrefl and irreflp as abbreviations
17 months ago, by desharna
tuned messages;
16 months ago, by wenzelm
tuned message;
16 months ago, by wenzelm
tuned messages and options;
16 months ago, by wenzelm
merged
16 months ago, by desharna
removed prod_set_conv attribute from top_empty_eq and top_empty_eq2
17 months ago, by desharna
discontinued "unzip" executable (see also eb96243a25c5 and 662de910a96b);
16 months ago, by wenzelm
more direct access to jEdit jar resources, without unzip;
16 months ago, by wenzelm
clarified check: allow to remove bad directories;
16 months ago, by wenzelm
clarified check;
16 months ago, by wenzelm
tuned message;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
proper unzip with strip option, within the JVM;
16 months ago, by wenzelm
updated to sqlite-jdbc-3.39.4.1;
16 months ago, by wenzelm
more standard component build process;
16 months ago, by wenzelm
clarified signature: prefer Scala functions instead of shell scripts;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
more direct target directory;
16 months ago, by wenzelm
clarified signature: prefer Scala functions instead of shell scripts;
16 months ago, by wenzelm
A new Isabelle/CTT example, and eliminated some old-style quotation marks
17 months ago, by paulson
clarified exception: avoid odd compiler warning;
17 months ago, by wenzelm
update to scala-3.2.1;
17 months ago, by wenzelm
recovered check from 69139cc01ba1: Windows does not support PosixFilePermission;
17 months ago, by wenzelm
update to jdk-17.0.5 (Oct-2022);
17 months ago, by wenzelm
more standard component build process;
17 months ago, by wenzelm
proper treatment of tar.gz double-extension;
17 months ago, by wenzelm
proper download, instead of assuming local directory;
17 months ago, by wenzelm
more standard component build process;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
discontinue unused JCEF: superseded by Electron with its bundled Chromium;
17 months ago, by wenzelm
prefer deterministic result;
17 months ago, by wenzelm
clarified command-line arguments: follow more recent isabelle build_XYZ;
17 months ago, by wenzelm
compile
17 months ago, by blanchet
correctly show '(> 2 s, timed out)' or similar in Sledgehammer's output
17 months ago, by blanchet
merged
17 months ago, by desharna
strengthened and renamed lemma reflp_on_equality
17 months ago, by desharna
renamed lemmas linorder.totalp_on_(ge|greater|le|less) and preorder.reflp_(ge|le)
17 months ago, by desharna
Added an example for Isabelle/CTT
17 months ago, by paulson
clarified signature;
17 months ago, by wenzelm
clarified signature: more explicit types;
17 months ago, by wenzelm
tuned output;
17 months ago, by wenzelm
prefer sorted result;
17 months ago, by wenzelm
separate style for re-use;
17 months ago, by wenzelm
ML support for the Prism.js syntax highlighter -- via Isabelle/Scala;
17 months ago, by wenzelm
retain data structures more accurately;
17 months ago, by wenzelm
proper join without delimiter;
17 months ago, by wenzelm
more accurate token types;
17 months ago, by wenzelm
clarified JS namespace;
17 months ago, by wenzelm
proper support for Windows;
17 months ago, by wenzelm
support for the Prism.js syntax highlighter -- via external Node.js process;
17 months ago, by wenzelm
support for JavaScript syntax and Node.js platform;
17 months ago, by wenzelm
merged
17 months ago, by wenzelm
tuned signature;
17 months ago, by wenzelm
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
17 months ago, by wenzelm
clarified signature: only support nameless separator;
17 months ago, by wenzelm
tuned signature;
17 months ago, by wenzelm
use timeout with MiniSat
17 months ago, by blanchet
merged
17 months ago, by desharna
added lemma reflp_on_conversp[simp]
17 months ago, by desharna
added lemma transp_reflclp[simp]
17 months ago, by desharna
added lemma reflclp_ident_if_reflp[simp]
17 months ago, by desharna
added lemma reflp_on_reflclp[simp]
17 months ago, by desharna
strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp
17 months ago, by desharna
more robust selection: avoid duplicates via "batch" number;
17 months ago, by wenzelm
tuned GUI;
17 months ago, by wenzelm
clarified GUI.Selector, with support for separator as pseudo-entry;
17 months ago, by wenzelm
clarified GUI state;
17 months ago, by wenzelm
clarified file names;
17 months ago, by wenzelm
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
17 months ago, by wenzelm
clarified signature: more public operations;
17 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
17 months ago, by wenzelm
merged
17 months ago, by nipkow
retain derived lemma for better findability
17 months ago, by nipkow
generalized sorted_sort_id to sort_key_id_if_sorted
17 months ago, by nipkow
suppress document_required GUI element for now: still unused;
17 months ago, by wenzelm
clarified layout;
17 months ago, by wenzelm
clarified node_required status: distinguish theory_required vs. document_required;
17 months ago, by wenzelm
proper user tool;
17 months ago, by wenzelm
tuned comments;
17 months ago, by wenzelm
support for EPTCS style with demo document;
17 months ago, by wenzelm
tuned message;
17 months ago, by wenzelm
clarified delay -- more reactive;
17 months ago, by wenzelm
provide Session.init_time as reference point for diagnostic messages;
17 months ago, by wenzelm
afford more reactive consolidation;
17 months ago, by wenzelm
minor performance tuning;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
afford unconditional presentation, notably export_theory and present_thy, notably for HTML + PDF presentation within PIDE;
17 months ago, by wenzelm
proper executable files for Windows;
17 months ago, by wenzelm
further attempts to confine dotnet to $ISABELLE_HOME_USER;
17 months ago, by wenzelm
tuned output;
17 months ago, by wenzelm
more command-line options;
17 months ago, by wenzelm
clarified component settings: always update existing version;
17 months ago, by wenzelm
more TODO for release;
17 months ago, by wenzelm
disable telemetry;
17 months ago, by wenzelm
clarified error;
17 months ago, by wenzelm
tuned message, example is in NEWS;
17 months ago, by wenzelm
proper default_platform;
17 months ago, by wenzelm
tuned NEWS;
17 months ago, by wenzelm
tuned message;
17 months ago, by wenzelm
support for Dotnet / Fsharp platform, via dynamically installed Isabelle component;
17 months ago, by wenzelm
tuned signature;
17 months ago, by wenzelm
tuned comments;
17 months ago, by wenzelm
clarified description, to fit better to e.g. "isabelle build_doc -a -V system jedit";
17 months ago, by wenzelm
clarified options: support lualatex as well, but prefer old pdflatex for demos;
17 months ago, by wenzelm
more command-line options;
17 months ago, by wenzelm
proper URL;
17 months ago, by wenzelm
document_build engine for "lipics", with options and document_files;
17 months ago, by wenzelm
clarified signature: allow to change options in instances of Document_Build.Engine;
17 months ago, by wenzelm
tuned signature;
17 months ago, by wenzelm
clarified options: LLNCS works with LuaLaTeX and Isabelle sections, although Springer might not like it;
17 months ago, by wenzelm
Better use the finite simproc selectively only
17 months ago, by nipkow
tuned document;
17 months ago, by wenzelm
tuned document;
17 months ago, by wenzelm
clarified LaTeX style;
17 months ago, by wenzelm
support for Springer LLNCS with demo document;
17 months ago, by wenzelm
prefer explicit utf8 for old pdflatex;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
proper chapter (amending 809cd1195795);
17 months ago, by wenzelm
merged
17 months ago, by wenzelm
tuned (again);
17 months ago, by wenzelm
prefer strict operation (see also f29056da5903);
17 months ago, by wenzelm
more antiquotations;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
prefer strict operation;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
tuned signature;
17 months ago, by wenzelm
tuned signature;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
misc tuning;
17 months ago, by wenzelm
clarified options;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
merged
17 months ago, by nipkow
added finite simproc
17 months ago, by nipkow
merged
17 months ago, by wenzelm
clarified directory layout: templates for user sessions;
17 months ago, by wenzelm
tuned proofs;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
proper pattern (amending 40a365360680);
17 months ago, by wenzelm
more timing;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
tuned comments;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
prefer abstract command kind (in contrast to 367f4512e65c);
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
tuned: avoid warning in IntelliJ IDEA;
17 months ago, by wenzelm
more accurate outer syntax keywords (see also 94b2690ad494): base session could be anything, e.g. ZF vs. HOL;
17 months ago, by wenzelm
tuned signature;
17 months ago, by wenzelm
clarified signature: do not require finished theory;
17 months ago, by wenzelm
clarified modules;
17 months ago, by wenzelm
merged
17 months ago, by desharna
added lemmas multp_mono_strong and mult_mono_strong
18 months ago, by desharna
merged
17 months ago, by wenzelm
support for FoilTeX with demo document;
17 months ago, by wenzelm
tuned comments;
17 months ago, by wenzelm
tuned whitespace for "isabelle doc" display;
17 months ago, by wenzelm
support for Easychair style with demo document;
17 months ago, by wenzelm
support for Dagstuhl LIPIcs style with demo document;
17 months ago, by wenzelm
clarified signature;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
clarified modules;
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
18 months ago, by wenzelm
restructured
18 months ago, by haftmann
modulus for polynomials is invariant wrt. units
18 months ago, by haftmann
proper Java syntax (amending ea79c21bcc47);
18 months ago, by wenzelm
reactivate emerging tool after release (see 322f2e2799a7);
18 months ago, by wenzelm
separate out definition of bound to avoid spurious sort hypotheses (by Jan van Brügge)
18 months ago, by traytel
merged
18 months ago, by paulson
Beautification of some declarations
18 months ago, by paulson
merged
18 months ago, by wenzelm
more robust etc/preferences: default value remains;
18 months ago, by wenzelm
formal bundling for Admin/build_release: avoid confusion about presence or absence in manual invocations;
18 months ago, by wenzelm
Beautifying CTT a tiny bit
18 months ago, by paulson
A couple of new theorems. Also additional coercions to the complex numbers
18 months ago, by paulson
more macOS platforms, without reference hardware;
18 months ago, by wenzelm
official release;
18 months ago, by wenzelm
merged
18 months ago, by wenzelm
Added tag Isabelle2022 for changeset 1ac2416e8432
18 months ago, by wenzelm
tuned signature (again, amending f32ac01aef5e), e.g. relevant for Isabelle/DOF;
Isabelle2022
18 months ago, by wenzelm
tuned signature, e.g. for Isabelle/DOF;
18 months ago, by wenzelm
updated to naproche-20221024: minor changes to documentation;
18 months ago, by wenzelm
Replaced some ugly legacy proofs
18 months ago, by paulson
more thorough cleanup;
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
tuned: more robust Scala syntax;
18 months ago, by wenzelm
merged
18 months ago, by wenzelm
no compression for database server: let PostgreSQL/TOAST do the job;
18 months ago, by wenzelm
prefer Zstd compression, notably for database exports;
18 months ago, by wenzelm
tuned: avoid redundant copy of potentially large array;
18 months ago, by wenzelm
merged
18 months ago, by desharna
tuned proof
18 months ago, by desharna
clarified signature;
18 months ago, by wenzelm
tuned signature, following isabelle.setup.Environment;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
clarified signature;
18 months ago, by wenzelm
prefer new instance, following "make" signature terminology;
18 months ago, by wenzelm
generic support for XZ and Zstd compression in Isabelle/Scala;
18 months ago, by wenzelm
clarified signature: default cache is actually dummy and not changed dynamically;
18 months ago, by wenzelm
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
18 months ago, by wenzelm
support for Zstd data compression;
18 months ago, by wenzelm
enforce fresh build;
18 months ago, by wenzelm
merged
18 months ago, by wenzelm
more robust read_file: prefer implicit replacement of bad input instead of failure via MalformedInputException;
18 months ago, by wenzelm
more informative errors, with optional exception trace as in Command_Line.tool;
18 months ago, by wenzelm
more robust reset of CLASSPATH: unset variable means "." in certain situations, e.g. scalac;
18 months ago, by wenzelm
proper chapter for each ROOT file (amending b07f2ff55144);
18 months ago, by wenzelm
tidying of ugly legacy proofs
18 months ago, by paulson
Tidying of old and ugly proofs
18 months ago, by paulson
deleted unused material
18 months ago, by paulson
A bit of tidying
18 months ago, by paulson
merged
18 months ago, by paulson
Slight tidying of legacy proofs
18 months ago, by paulson
merged
18 months ago, by wenzelm
update naproche component;
18 months ago, by wenzelm
Added tag Isabelle2022-RC4 for changeset 8b4108f41c77
18 months ago, by wenzelm
rebuild with proper Isabelle version;
18 months ago, by wenzelm
removed junk;
18 months ago, by wenzelm
more robust, e.g. for "isabelle dump";
18 months ago, by wenzelm
more robust, e.g. for "isabelle dump";
18 months ago, by wenzelm
more robust, e.g. for "isabelle dump";
18 months ago, by wenzelm
allow spaces in SCALA_HOME directory name;
18 months ago, by wenzelm
avoid spurious error messages, e.g. when scala is missing;
18 months ago, by wenzelm
more NEWS;
18 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
18 months ago, by wenzelm
avoid result based on outdated state, e.g. relevant for use_theories with changed files;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
18 months ago, by wenzelm
more robust treatment of state and events;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
proper result state (amending 954640e846d6);
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
tuned: clarified old_theory (in contrast to 4d5342898b1);
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
more robust: active consumer for check_state/check_progress;
18 months ago, by wenzelm
proper update of non-committed theories (see also 2bf1d0e57695, 2a1583baaaa0);
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with symbols like \<^here>;
18 months ago, by wenzelm
merged
18 months ago, by desharna
added lemma fmember_iff_member_fset
18 months ago, by desharna
tiny renaming
18 months ago, by paulson
merged
18 months ago, by paulson
Added the multiset termination proof
18 months ago, by paulson
generate some metainformation not only for SPASS but also for Zipperposition, for experimentation
18 months ago, by blanchet
added lemma wfP_subset_mset[simp]
18 months ago, by desharna
Tidying of some very old proofs
18 months ago, by paulson
merged
18 months ago, by paulson
tidying of some old proofs
18 months ago, by paulson
merged
18 months ago, by nipkow
new contributor
18 months ago, by nipkow
more List lemmas (partly by Jeremy Sylvestre)
18 months ago, by nipkow
merged
18 months ago, by paulson
merged
18 months ago, by paulson
Trying to clean up some messy proofs
18 months ago, by paulson
Mostly, removing the unfold method
18 months ago, by paulson
Mostly trivial simplifications
18 months ago, by paulson
Removal of the "unfold" method in favour of "unfolding"
18 months ago, by paulson
Elimination of the archaic ASCII syntax
18 months ago, by paulson
strengthened lemmas preorder.reflp_ge[simp] and preorder.reflp_le[simp]
18 months ago, by desharna
added lemmas linorder.totalp_ge[simp], linorder.totalp_greater[simp], linorder.totalp_le[simp], and linorder.totalp_less[simp]
18 months ago, by desharna
NEWS
18 months ago, by desharna
merged
18 months ago, by desharna
fixed NEWS following cee0b9fccf6f
18 months ago, by desharna
renamed lemma inj_on_strict_subset to image_strict_mono for symmetry with image_mono and to distinguish from inj_on_subset
18 months ago, by desharna
merged
18 months ago, by wenzelm
proper Deps.is_empty (amending 77327455b00d), e.g. relevant for warning "Nothing to build";
18 months ago, by wenzelm
tuned whitespace;
18 months ago, by wenzelm
less ambitious Bytes.chunk_size, which is presumably more stable with memory management under heavy load;
18 months ago, by wenzelm
tuned comment;
18 months ago, by wenzelm
support for system option ML_system_apple: emulated x86_64 Poly/ML is sometimes more stable than native ARM64;
18 months ago, by wenzelm
updated to repository version polyml-test-bafe319bc3a6, which is presumably more stable (especially for ARM64);
18 months ago, by wenzelm
more robust: prefer Windows $USERNAME;
18 months ago, by wenzelm
proper home directory for ssh configuration (e.g. ~/.ssh/config);
18 months ago, by wenzelm
more NEWS;
18 months ago, by wenzelm
clarified signature: more arguments;
18 months ago, by wenzelm
added lemma fimage_strict_mono
18 months ago, by desharna
added lemma wfP_pfsubset
18 months ago, by desharna
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
18 months ago, by desharna
update components.sha1;
18 months ago, by wenzelm
proper description;
18 months ago, by wenzelm
one more lemma
18 months ago, by nipkow
merged
18 months ago, by nipkow
adjusted proofs
18 months ago, by nipkow
added and reorganized lemmas (some suggested by Jeremy Sylvestre)
18 months ago, by nipkow
removed redundant lemma
18 months ago, by nipkow
moved theorem from Fun to Set
18 months ago, by nipkow
added lemmas antisymp_ge[simp], antisymp_greater[simp], antisymp_le[simp], and antisymp_less[simp]
18 months ago, by desharna
added lemmas reflp_ge[simp] and reflp_le[simp]
18 months ago, by desharna
removed unused universal variable from lemma reflp_onI
18 months ago, by desharna
added lemmas irreflD and irreflpD
18 months ago, by desharna
added lemmas antisym_if_asym and antisymp_if_asymp
18 months ago, by desharna
strengthened lemma total_on_singleton and added lemma totalp_on_singleton
18 months ago, by desharna
generalized type classes as suggested by Jeremy Sylvestre
18 months ago, by nipkow
euclidean division on gaussian numbers
18 months ago, by haftmann
tuned proof
18 months ago, by haftmann
note on signed division on words
18 months ago, by haftmann
tuned definition
18 months ago, by haftmann
spelling
18 months ago, by haftmann
tuned proof
18 months ago, by haftmann
slightly less abusive proof pattern
18 months ago, by haftmann
back to post-release mode -- after fork point;
18 months ago, by wenzelm
Added tag Isabelle2022-RC3 for changeset d704efeb01db
18 months ago, by wenzelm
proper cygwin component (see d042947e47a3)
18 months ago, by wenzelm
proper base names;
18 months ago, by wenzelm
suppress command echo in output;
18 months ago, by wenzelm
include openssh for rsync (see also a1c7829ac2de);
18 months ago, by wenzelm
provide naproche-20221002;
18 months ago, by wenzelm
merged
18 months ago, by wenzelm
clarified signature: more operations;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
18 months ago, by wenzelm
clarified signature, to support external tools like "isabelle narration";
18 months ago, by wenzelm
syntactic type classes for signed division operators
18 months ago, by haftmann
reduce prominence of facts
19 months ago, by haftmann
clarified signature;
19 months ago, by wenzelm
more explanations on the new order prover (based on 10945fc183cd), without violating strict monotonicity of NEWS wrt. official releases;
19 months ago, by wenzelm
restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;
19 months ago, by wenzelm
added documentation about new order prover
19 months ago, by Lukas Stevens
tweaked
19 months ago, by Lukas Stevens
tweaked;
19 months ago, by Fabian Huch
moved relevant theorems from theory Divides to theory Euclidean_Division
19 months ago, by haftmann
amend jenkins ci build;
19 months ago, by Fabian Huch
restructured ci profile into modular ci build system;
19 months ago, by Fabian Huch
more structured proofs
19 months ago, by paulson
fixed some theory presentation issues (?)
19 months ago, by paulson
recover informal "&" from 0c18df79b1c8;
19 months ago, by wenzelm
added a couple of structured proofs
19 months ago, by paulson
More obsolete "unfold" calls
19 months ago, by paulson
getting rid of apply (unfold ...)
19 months ago, by paulson
More syntactic cleanup. LaTeX markup working
19 months ago, by paulson
more modernisation of syntax
19 months ago, by paulson
Removal of obsolete ASCII syntax
19 months ago, by paulson
clarified options;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
provide missing LaTeX macro, e.g. for AFP/PAC_Checker;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
streamlined division on polynomials
19 months ago, by haftmann
streamlined division on polynomials
19 months ago, by haftmann
clarified signature: re-use store/cache from build results;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified signature: persistent Node.source / Snapshot.source;
19 months ago, by wenzelm
more examples;
19 months ago, by wenzelm
proper filter (amending fb4215da4919);
19 months ago, by wenzelm
clarified conditions: no_build is ok for presentation if "all_current" holds;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified presentation_sessions: work with partial results;
19 months ago, by wenzelm
tuned signature: removed unused operations;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned comments;
19 months ago, by wenzelm
streamlined division on polynomials
19 months ago, by haftmann
clarified packaging;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
Added tag Isabelle2022-RC2 for changeset 778152d51e97
19 months ago, by wenzelm
show SSH options in PIDE GUI;
19 months ago, by wenzelm
inplace update: proper Linux version;
19 months ago, by wenzelm
provide naproche-20220917;
19 months ago, by wenzelm
clarified NEWS;
19 months ago, by wenzelm
proper platform directory x86_64-linux, to have it purged for other platforms;
19 months ago, by wenzelm
MLton component for x86_64-linux;
19 months ago, by wenzelm
clarified Docker base image;
19 months ago, by wenzelm
proper file headers;
19 months ago, by wenzelm
tuned messages;
19 months ago, by wenzelm
support for ISABELLE_MLTON_OPTIONS, notably for Ubuntu 22.04 with external mlton executable;
19 months ago, by wenzelm
omit menu for unfinished tool;
19 months ago, by wenzelm
include ssh + rsync as required for Isabelle tools, e.g. "isabelle sync";
19 months ago, by wenzelm
more robust: snap version of docker cannot access /tmp;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
update to scala-3.2.0;
19 months ago, by wenzelm
avoid crash of JLine on Windows;
19 months ago, by wenzelm
update to jdk-17.0.4.1+1 from 22-Aug-2022 (https://docs.azul.com/core/zulu-openjdk/release-notes/11.58-17.36-august-2022);
19 months ago, by wenzelm
clarified default, following 8b695e59db3f;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
19 months ago, by wenzelm
clarified options;
19 months ago, by wenzelm
clarified options;
19 months ago, by wenzelm
discontinued unclear timeout (stemming from jEdit JSch setup, see 14782d58a503), to make it work with native Windows ssh.exe;
19 months ago, by wenzelm
proper time values in seconds;
19 months ago, by wenzelm
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
19 months ago, by wenzelm
more robust, notably for macOS (see also ff92d6edff2c);
19 months ago, by wenzelm
back to plain /tmp (despite 1df53737c59b): relevant for ssh on macOS, to avoid error "unix_listener: path too long for Unix domain socket";
19 months ago, by wenzelm
tuned names;
19 months ago, by wenzelm
proper order of platforms, to make it work uniformly on all plaform families;
19 months ago, by wenzelm
more portable;
19 months ago, by wenzelm
build both arm64-darwin and x86_64-darwin on Apple ARM hardware;
19 months ago, by wenzelm
unused;
19 months ago, by wenzelm
tuned message;
19 months ago, by wenzelm
more items;
19 months ago, by wenzelm
more robust: do not assume Bash syntax while testing for it;
19 months ago, by wenzelm
obsolete;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
proper treatment of complex multi-line script;
19 months ago, by wenzelm
more robust;
19 months ago, by wenzelm
more robust: Bash.string operations require remote bash;
19 months ago, by wenzelm
support port forwarding without multiplexing (for the sake of Windows);
19 months ago, by wenzelm
misc tuning and clarification;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
More on division concerning gauss numbers.
19 months ago, by haftmann
more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier;
19 months ago, by wenzelm
more concise instance-specific rules on euclidean relation
19 months ago, by haftmann
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
20 months ago, by paulson
Three new theorems about real polynomial functions
20 months ago, by paulson
tuned GUI;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified GUI behaviour;
20 months ago, by wenzelm
eliminated odd Unicode blanks;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
eliminated DOS line endings;
20 months ago, by wenzelm
eliminated tabs, assuming tab-width=8;
20 months ago, by wenzelm
eliminated tabs, assuming tab-width=4;
20 months ago, by wenzelm
updated to current Cygwin, near 3.3.5-1;
20 months ago, by wenzelm
test macOS 12 Monterey via laramac01;
20 months ago, by wenzelm
clarified GUI update;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
more GUI functionality;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified component structure, concerning initialization order;
20 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;
20 months ago, by wenzelm
provide cvc5-1.0.2 (inactive);
20 months ago, by wenzelm
tuned output;
20 months ago, by wenzelm
tool to build Isabelle component for cvc5;
20 months ago, by wenzelm
tuned: avoid odd stateful programming;
20 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
clarified signature;
20 months ago, by wenzelm
more robust directory structure: always relative to session_dir;
20 months ago, by wenzelm
discontinued slightly odd integrity check (from af2d0e07493b): requires a different approach;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
misc tuning and clarification;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature: replaced Sessions.Deps by Sessions.Structure from HTML_Context;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified signature: avoid constants from Sessions.Structure within Session.Base;
20 months ago, by wenzelm
clarified signature: avoid object-oriented HTML_Context;
20 months ago, by wenzelm
tuned type signature
20 months ago, by haftmann
tuned type signature
20 months ago, by haftmann
streamlined theorems
20 months ago, by haftmann
more thorough split rules for div and mod on numerals, tuned split rules setup
20 months ago, by haftmann
streamlined simpset building, avoiding duplicated rewrite rules
20 months ago, by haftmann
consolidated attribute name
20 months ago, by haftmann
streamlined theorems
20 months ago, by haftmann
streamlined theorems and sections
20 months ago, by haftmann
streamlined primitive definitions for integer division
20 months ago, by haftmann
reintroduced SPASS to the mix
20 months ago, by blanchet
tweaked generation of Isar proofs
20 months ago, 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
20 months ago, by blanchet
tuned comments;
20 months ago, by wenzelm
updated to sumatra_pdf-3.4.6;
20 months ago, 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;
20 months ago, by wenzelm
revived 'try0' and 'smart' Isar proofs in Sledgehammer
20 months ago, by blanchet
Cleanup of NonstandardAnalysis
20 months ago, by paulson
A bit of cleaning up
20 months ago, by paulson
The same, without adding a new simprule
20 months ago, by paulson
moved some material from Sum_of_Powers
20 months ago, by paulson
merged
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified theory_names with exported content;
20 months ago, by wenzelm
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
20 months ago, by wenzelm
proper treatment of empty lines (amending 08f89f0e8a62);
20 months ago, by wenzelm
clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);
20 months ago, by wenzelm
merged
20 months ago, by paulson
The right way to formulate card_UNION, plus the old version for compatibility
20 months ago, by paulson
tuned comments;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature: more explicit types;
20 months ago, by wenzelm
clarified signature --- avoid dependent types;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
clarified signature: avoid public representation;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
20 months ago, by wenzelm
clarified signature: more explicit types;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
tuned, following 298707451ec2;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
clarified signature: more explicit types;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
more GUI elements;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
clarified signature --- more operations;
20 months ago, by wenzelm
clarified signature --- simplified types;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
proper toString for Content_XML, which is not covered by trait Content;
20 months ago, by wenzelm
clarified output;
20 months ago, by wenzelm
clarified signature: support different document_session, e.g. within running PIDE session;
20 months ago, by wenzelm
unused (despite cf52379c0776);
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
unused (see 696819fe2424);
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
basic setup for document build panel;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
tip