| Fri, 25 Jun 2021 12:53:56 +0200 |
wenzelm |
updated to flatlaf-1.2;
|
changeset |
files
|
| Fri, 25 Jun 2021 12:52:54 +0200 |
wenzelm |
proper directories after reinstallation of lxbroy10;
|
changeset |
files
|
| Fri, 25 Jun 2021 12:32:56 +0200 |
wenzelm |
more visual emphasis on node status;
|
changeset |
files
|
| Thu, 24 Jun 2021 06:06:32 +0000 |
haftmann |
more word cleanup
|
changeset |
files
|
| Wed, 23 Jun 2021 18:38:37 +0000 |
haftmann |
merged
|
changeset |
files
|
| Wed, 23 Jun 2021 17:43:31 +0000 |
haftmann |
more default simp rules
|
changeset |
files
|
| Wed, 23 Jun 2021 17:43:31 +0000 |
haftmann |
some word streamlining
|
changeset |
files
|
| Wed, 23 Jun 2021 17:39:43 +0200 |
wenzelm |
avoid legacy domain informatik.tu-muenchen.de;
|
changeset |
files
|
| Fri, 18 Jun 2021 15:03:12 +0200 |
wenzelm |
tuned --- following hints by IntelliJ;
|
changeset |
files
|
| Fri, 18 Jun 2021 14:35:48 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 18 Jun 2021 12:13:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 18 Jun 2021 12:13:09 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 18 Jun 2021 12:12:28 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 18 Jun 2021 11:48:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 18 Jun 2021 11:32:32 +0200 |
wenzelm |
tuned signature (see 2d6a489adb01);
|
changeset |
files
|
| Thu, 17 Jun 2021 12:57:22 +0200 |
desharna |
added support for TFX's and THF's $ite to Sledgehammer
|
changeset |
files
|
| Thu, 17 Jun 2021 11:27:21 +0200 |
desharna |
tuned Mirabelle documentation
|
changeset |
files
|
| Thu, 17 Jun 2021 10:46:27 +0200 |
desharna |
shortened long lines
|
changeset |
files
|
| Thu, 17 Jun 2021 10:43:53 +0200 |
desharna |
fixed typos
|
changeset |
files
|
| Thu, 17 Jun 2021 10:37:29 +0200 |
desharna |
updated Mirabelle documentation
|
changeset |
files
|
| Thu, 17 Jun 2021 10:30:07 +0200 |
desharna |
changed Mirabelle's filter to use short theory names
|
changeset |
files
|
| Wed, 16 Jun 2021 08:19:09 +0000 |
haftmann |
more lemmas
|
changeset |
files
|
| Sat, 12 Jun 2021 15:37:25 +0200 |
desharna |
added support for unbounded max calls to Mirabelle
|
changeset |
files
|
| Sat, 12 Jun 2021 12:39:33 +0200 |
desharna |
added warnings when defining unamed or redefining Mirabelle action
|
changeset |
files
|
| Sat, 12 Jun 2021 12:16:19 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 11 Jun 2021 09:33:43 +0200 |
desharna |
tuned Mirabelle
|
changeset |
files
|
| Thu, 10 Jun 2021 11:54:14 +0200 |
desharna |
merged
|
changeset |
files
|
| Thu, 10 Jun 2021 11:21:57 +0200 |
desharna |
refactored Mirabelle to produce output in real time
|
changeset |
files
|
| Wed, 09 Jun 2021 18:04:22 +0000 |
haftmann |
global interpretation into nested targets
|
changeset |
files
|
| Wed, 09 Jun 2021 18:04:21 +0000 |
haftmann |
more succint interfaces
|
changeset |
files
|
| Wed, 09 Jun 2021 11:25:21 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 09 Jun 2021 11:21:42 +0200 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Wed, 09 Jun 2021 10:58:28 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Wed, 09 Jun 2021 10:52:37 +0200 |
wenzelm |
proper profiling within command execution: messages require PIDE id;
|
changeset |
files
|
| Wed, 09 Jun 2021 10:37:53 +0200 |
wenzelm |
more systematic treatment of profiling mode;
|
changeset |
files
|
| Tue, 08 Jun 2021 23:36:30 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Tue, 08 Jun 2021 23:34:06 +0200 |
wenzelm |
prefer less intrusive tracing message;
|
changeset |
files
|
| Tue, 08 Jun 2021 23:23:59 +0200 |
wenzelm |
clarified documentation: tracing messages are not shown here;
|
changeset |
files
|
| Tue, 08 Jun 2021 16:32:57 +0200 |
wenzelm |
add missing file;
|
changeset |
files
|
| Tue, 08 Jun 2021 13:17:45 +0200 |
wenzelm |
more formal ML profiling messages;
|
changeset |
files
|
| Mon, 07 Jun 2021 16:40:26 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Tue, 08 Jun 2021 17:01:32 +0200 |
nipkow |
Lukas Steven's more general fold foctions for maps
|
changeset |
files
|
| Tue, 01 Jun 2021 19:46:34 +0200 |
nipkow |
More general fold function for maps
|
changeset |
files
|
| Mon, 07 Jun 2021 15:13:34 +0200 |
wenzelm |
follow Phabricator update 2021 Week 23;
|
changeset |
files
|
| Mon, 07 Jun 2021 14:41:04 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 07 Jun 2021 14:40:22 +0200 |
wenzelm |
more formal theory and session names;
|
changeset |
files
|
| Mon, 07 Jun 2021 14:34:55 +0200 |
wenzelm |
proper NEWS after Isabelle2021;
|
changeset |
files
|
| Mon, 07 Jun 2021 13:04:17 +0200 |
wenzelm |
updated descriptions;
|
changeset |
files
|
| Mon, 07 Jun 2021 11:42:05 +0200 |
wenzelm |
allow system option short form NAME for NAME=true for type string, not just bool;
|
changeset |
files
|
| Mon, 07 Jun 2021 09:36:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 07 Jun 2021 09:27:01 +0200 |
wenzelm |
more robust within session "HOL";
|
changeset |
files
|
| Sun, 06 Jun 2021 21:39:26 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 06 Jun 2021 21:17:23 +0200 |
wenzelm |
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
|
changeset |
files
|
| Sun, 06 Jun 2021 20:29:52 +0200 |
wenzelm |
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
|
changeset |
files
|
| Sun, 06 Jun 2021 16:34:57 +0200 |
wenzelm |
refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;
|
changeset |
files
|
| Sun, 06 Jun 2021 14:55:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 06 Jun 2021 14:52:56 +0200 |
wenzelm |
more uniform schedule_theories, notably for "present" and "commit" phase after loading;
|
changeset |
files
|
| Sun, 06 Jun 2021 14:12:00 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 06 Jun 2021 15:49:39 +0000 |
haftmann |
moved more legacy to AFP
|
changeset |
files
|
| Sat, 05 Jun 2021 21:01:00 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sat, 05 Jun 2021 20:20:25 +0200 |
wenzelm |
clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);
|
changeset |
files
|
| Sat, 05 Jun 2021 20:15:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 05 Jun 2021 19:21:29 +0200 |
wenzelm |
more thorough update of required files (amending 1529c3eb6bac);
|
changeset |
files
|
| Sat, 05 Jun 2021 12:57:52 +0200 |
wenzelm |
clarified examples;
|
changeset |
files
|
| Sat, 05 Jun 2021 12:45:00 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 05 Jun 2021 12:29:57 +0200 |
wenzelm |
misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a);
|
changeset |
files
|
| Fri, 04 Jun 2021 23:55:35 +0200 |
wenzelm |
tuned --- reduced source complexity;
|
changeset |
files
|
| Fri, 04 Jun 2021 23:40:44 +0200 |
wenzelm |
proper usage (amending f7ea394490f5);
|
changeset |
files
|
| Fri, 04 Jun 2021 23:37:27 +0200 |
wenzelm |
merged, resolving minor conflict;
|
changeset |
files
|
| Fri, 04 Jun 2021 23:30:46 +0200 |
wenzelm |
allow build session setup, e.g. for protocol handlers;
|
changeset |
files
|
| Fri, 04 Jun 2021 22:58:38 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Fri, 04 Jun 2021 22:50:32 +0200 |
wenzelm |
tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated);
|
changeset |
files
|
| Fri, 04 Jun 2021 22:46:11 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 04 Jun 2021 22:30:17 +0200 |
wenzelm |
removed pointless option (see 3d0952893db8);
|
changeset |
files
|
| Fri, 04 Jun 2021 22:01:16 +0200 |
wenzelm |
tuned --- avoid redundant future tasks from already loaded theories;
|
changeset |
files
|
| Fri, 04 Jun 2021 21:46:14 +0200 |
wenzelm |
no comment --- topological order appears to be fine since 04-Mar-2013;
|
changeset |
files
|
| Fri, 04 Jun 2021 21:36:42 +0200 |
wenzelm |
more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7);
|
changeset |
files
|
| Fri, 04 Jun 2021 23:03:12 +0200 |
desharna |
moved stride option from sledgehammer action to main mirabelle
|
changeset |
files
|
| Thu, 03 Jun 2021 10:58:15 +0100 |
paulson |
merged
|
changeset |
files
|
| Thu, 03 Jun 2021 10:47:20 +0100 |
paulson |
new lemmas mostly about paths
|
changeset |
files
|
| Wed, 02 Jun 2021 12:45:27 +0000 |
haftmann |
lexorders the locale way
|
changeset |
files
|
| Mon, 31 May 2021 20:27:45 +0000 |
haftmann |
more accurate export morphism enables proper instantiation by interpretation
|
changeset |
files
|
| Sat, 29 May 2021 13:42:26 +0100 |
paulson |
merged
|
changeset |
files
|
| Fri, 28 May 2021 18:11:34 +0100 |
paulson |
some new and/or varient results about images
|
changeset |
files
|
| Fri, 28 May 2021 14:43:06 +0100 |
paulson |
nicer statement of Liouville_theorem
|
changeset |
files
|
| Fri, 28 May 2021 20:21:25 +0000 |
haftmann |
more lemmas
|
changeset |
files
|
| Fri, 28 May 2021 20:21:23 +0000 |
haftmann |
max word moved to Word_Lib in AFP
|
changeset |
files
|
| Wed, 26 May 2021 18:07:49 +0200 |
wenzelm |
more robust syntax;
|
changeset |
files
|
| Tue, 25 May 2021 23:58:49 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Tue, 25 May 2021 23:37:32 +0200 |
wenzelm |
clarified document export names;
|
changeset |
files
|
| Tue, 25 May 2021 23:18:29 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 25 May 2021 23:12:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 25 May 2021 23:04:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 25 May 2021 23:00:29 +0200 |
wenzelm |
avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;
|
changeset |
files
|
| Tue, 25 May 2021 22:28:39 +0200 |
wenzelm |
compose Latex text as XML, output exported YXML in Isabelle/Scala;
|
changeset |
files
|
| Tue, 25 May 2021 21:44:01 +0200 |
wenzelm |
more direct index_entry: no positions required -- text is eventually moved to .ind file;
|
changeset |
files
|
| Tue, 25 May 2021 21:32:21 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 24 May 2021 11:58:06 +0200 |
wenzelm |
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
|
changeset |
files
|
| Sun, 23 May 2021 23:15:04 +0200 |
wenzelm |
tuned message, e.g. for Pure bootstrap;
|
changeset |
files
|
| Sun, 23 May 2021 23:00:10 +0200 |
wenzelm |
proper signature export (amending b50f8cc8c08e);
|
changeset |
files
|
| Sun, 23 May 2021 22:46:30 +0200 |
wenzelm |
syslog option for "isabelle build";
|
changeset |
files
|
| Sun, 23 May 2021 21:03:32 +0200 |
wenzelm |
further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea);
|
changeset |
files
|
| Sun, 23 May 2021 20:34:43 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 23 May 2021 20:12:36 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Sun, 23 May 2021 19:59:37 +0200 |
wenzelm |
clarified index, more like formal @{element_ref};
|
changeset |
files
|
| Sun, 23 May 2021 19:29:18 +0200 |
wenzelm |
clarified treatment of type constructors;
|
changeset |
files
|
| Sun, 23 May 2021 18:04:35 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sun, 23 May 2021 17:35:28 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 23 May 2021 17:08:34 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Sat, 22 May 2021 22:58:10 +0200 |
wenzelm |
more uniform document antiquotations for ML: consolidate former setup for manuals;
|
changeset |
files
|
| Sat, 22 May 2021 21:52:13 +0200 |
wenzelm |
clarified names;
|
changeset |
files
|
| Sat, 22 May 2021 13:35:25 +0200 |
wenzelm |
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
|
changeset |
files
|
| Fri, 21 May 2021 13:07:53 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Fri, 21 May 2021 12:29:29 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Fri, 21 May 2021 11:19:53 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 May 2021 10:15:38 +0200 |
wenzelm |
clarified signature: avoid dispatch via name;
|
changeset |
files
|
| Thu, 20 May 2021 23:33:54 +0200 |
wenzelm |
clarified, e.g. type variables;
|
changeset |
files
|
| Thu, 20 May 2021 22:02:19 +0200 |
wenzelm |
tuned index;
|
changeset |
files
|
| Thu, 20 May 2021 21:21:37 +0200 |
wenzelm |
more ambitious default for index "is like";
|
changeset |
files
|
| Thu, 20 May 2021 18:32:59 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 20 May 2021 18:16:13 +0200 |
wenzelm |
support for index entries;
|
changeset |
files
|
| Thu, 20 May 2021 13:56:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 20 May 2021 13:50:20 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 19 May 2021 21:42:45 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Wed, 19 May 2021 18:22:56 +0200 |
wenzelm |
clarified old document build;
|
changeset |
files
|
| Wed, 19 May 2021 16:44:40 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Wed, 19 May 2021 16:41:32 +0200 |
wenzelm |
prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee;
|
changeset |
files
|
| Wed, 19 May 2021 16:35:10 +0200 |
wenzelm |
prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document;
|
changeset |
files
|
| Wed, 19 May 2021 15:53:55 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Wed, 19 May 2021 15:45:13 +0200 |
wenzelm |
proper Unix lines;
|
changeset |
files
|
| Wed, 19 May 2021 13:21:08 +0200 |
wenzelm |
prefer explicit option document_bibliography (actually ignored by build script);
|
changeset |
files
|
| Wed, 19 May 2021 13:19:37 +0200 |
wenzelm |
explicit option document_bibliography;
|
changeset |
files
|
| Wed, 19 May 2021 12:53:51 +0200 |
wenzelm |
proper bibliography;
|
changeset |
files
|
| Wed, 19 May 2021 13:00:42 +0200 |
wenzelm |
discontinued obsolete "isabelle latex";
|
changeset |
files
|
| Wed, 19 May 2021 11:54:58 +0200 |
wenzelm |
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
|
changeset |
files
|
| Wed, 19 May 2021 11:48:35 +0200 |
wenzelm |
default document_build (lualatex);
|
changeset |
files
|
| Wed, 19 May 2021 11:18:38 +0200 |
wenzelm |
more robust: allow \printindex within the document;
|
changeset |
files
|
| Wed, 19 May 2021 11:15:13 +0200 |
wenzelm |
clarified bash scripts, with public interfaces for user-defined Document_Build.Engine;
|
changeset |
files
|
| Wed, 19 May 2021 10:41:28 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 18 May 2021 22:02:21 +0200 |
wenzelm |
option document_preprocessor;
|
changeset |
files
|
| Tue, 18 May 2021 21:09:51 +0200 |
wenzelm |
show symbols in Isabelle/ML instead of perl;
|
changeset |
files
|
| Tue, 18 May 2021 20:19:02 +0200 |
wenzelm |
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
|
changeset |
files
|
| Tue, 18 May 2021 19:59:22 +0200 |
wenzelm |
tuned --- more robust;
|
changeset |
files
|
| Tue, 18 May 2021 19:49:06 +0200 |
wenzelm |
discontinued somewhat pointless "fixbookmarks": default output works sufficiently well;
|
changeset |
files
|
| Tue, 18 May 2021 17:19:19 +0200 |
wenzelm |
more uniform bibtex error, without using perl (see 4710dd5093a3);
|
changeset |
files
|
| Tue, 18 May 2021 17:02:45 +0200 |
wenzelm |
proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error);
|
changeset |
files
|
| Tue, 18 May 2021 16:18:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 18 May 2021 16:15:19 +0200 |
wenzelm |
clarified command-line options;
|
changeset |
files
|
| Tue, 18 May 2021 16:01:01 +0200 |
wenzelm |
obsolete (see 5a3a2a52648d);
|
changeset |
files
|
| Tue, 18 May 2021 15:57:49 +0200 |
wenzelm |
redundant: copy produced from session document_files;
|
changeset |
files
|
| Tue, 18 May 2021 15:46:03 +0200 |
wenzelm |
clarified treatment of Isabelle .sty files;
|
changeset |
files
|
| Tue, 18 May 2021 15:17:55 +0200 |
wenzelm |
option document_logo;
|
changeset |
files
|
| Mon, 17 May 2021 23:38:16 +0200 |
wenzelm |
proper options;
|
changeset |
files
|
| Mon, 17 May 2021 23:30:25 +0200 |
wenzelm |
option document_build refers to build engine in Isabelle/Scala;
|
changeset |
files
|
| Mon, 17 May 2021 20:37:42 +0200 |
wenzelm |
redundant: tmp_dir is purged anyway;
|
changeset |
files
|
| Mon, 17 May 2021 20:32:52 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Mon, 17 May 2021 16:15:25 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 17 May 2021 15:01:37 +0200 |
wenzelm |
tuned --- clarified corner cases;
|
changeset |
files
|
| Mon, 17 May 2021 14:54:03 +0200 |
wenzelm |
more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases;
|
changeset |
files
|
| Mon, 17 May 2021 14:07:51 +0200 |
wenzelm |
clarified signature -- avoid odd warning about scala/bug#6675;
|
changeset |
files
|
| Mon, 17 May 2021 14:07:13 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 17 May 2021 13:48:20 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 17 May 2021 13:40:01 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 17 May 2021 13:37:47 +0200 |
wenzelm |
proper syntax of Scala 3;
|
changeset |
files
|
| Sun, 16 May 2021 23:22:03 +0200 |
wenzelm |
enforce syntax of Scala 3;
|
changeset |
files
|
| Wed, 19 May 2021 14:17:40 +0100 |
paulson |
things need to be ugly
|
changeset |
files
|
| Tue, 18 May 2021 20:25:19 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 18 May 2021 20:25:08 +0100 |
paulson |
sorted as an abbreviation
|
changeset |
files
|
| Mon, 17 May 2021 09:07:30 +0000 |
haftmann |
mere abbreviation for logical alias
|
changeset |
files
|
| Mon, 17 May 2021 13:57:19 +1000 |
kleing |
avoid unexpected output+behaviour when CDPATH is set
|
changeset |
files
|
| Sun, 16 May 2021 19:37:15 +0200 |
wenzelm |
recover some Linux test, using old macbroy2 as i21of4 (Ubuntu 20.04);
|
changeset |
files
|
| Sun, 16 May 2021 16:05:13 +0200 |
wenzelm |
avoid perl;
|
changeset |
files
|
| Sun, 16 May 2021 13:34:27 +0200 |
wenzelm |
tuned signature --- following hints by IntelliJ IDEA;
|
changeset |
files
|
| Sun, 16 May 2021 13:14:16 +0200 |
wenzelm |
ignore session build timeout, notably in AFP;
|
changeset |
files
|
| Sun, 16 May 2021 13:06:13 +0200 |
wenzelm |
check timeout_ignored as in ML, before applying timeout_scale;
|
changeset |
files
|
| Sat, 15 May 2021 22:39:07 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 15 May 2021 22:36:36 +0200 |
wenzelm |
proper build of required session images vs. build with Mirabelle presentation;
|
changeset |
files
|
| Sat, 15 May 2021 22:06:05 +0200 |
wenzelm |
reactive "sledgehammer";
|
changeset |
files
|
| Sat, 15 May 2021 17:40:36 +0200 |
wenzelm |
reactive "sledgehammer_filter": statically correct, but untested (no proof_file);
|
changeset |
files
|
| Sat, 15 May 2021 17:38:49 +0200 |
wenzelm |
clarified command-line;
|
changeset |
files
|
| Sat, 15 May 2021 13:25:52 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 15 May 2021 12:33:08 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 15 May 2021 12:25:24 +0200 |
wenzelm |
clarified log content;
|
changeset |
files
|
| Fri, 14 May 2021 21:32:11 +0200 |
wenzelm |
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
|
changeset |
files
|
| Thu, 13 May 2021 15:52:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 13 May 2021 15:38:52 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Wed, 12 May 2021 17:17:46 +0200 |
wenzelm |
unused (see 8ffc607c345d);
|
changeset |
files
|
| Wed, 12 May 2021 16:47:52 +0200 |
wenzelm |
clarified signature: provide access to previous state;
|
changeset |
files
|
| Wed, 12 May 2021 14:55:51 +0200 |
wenzelm |
clarified signature (see Scala version);
|
changeset |
files
|
| Wed, 12 May 2021 13:10:13 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 12 May 2021 12:22:44 +0200 |
wenzelm |
avoid duplicate loading of ML file;
|
changeset |
files
|
| Fri, 14 May 2021 12:43:19 +0100 |
paulson |
strict_sorted now an abbreviation
|
changeset |
files
|
| Wed, 12 May 2021 17:05:29 +0000 |
haftmann |
explicit type class operations for type-specific implementations
|
changeset |
files
|
| Wed, 12 May 2021 17:05:28 +0000 |
haftmann |
obsolete
|
changeset |
files
|
| Wed, 12 May 2021 09:31:18 +0200 |
desharna |
added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran
|
changeset |
files
|
| Wed, 12 May 2021 06:35:16 +0200 |
nipkow |
merged
|
changeset |
files
|
| Tue, 11 May 2021 22:40:59 +0200 |
nipkow |
generalized type
|
changeset |
files
|
| Tue, 11 May 2021 21:57:43 +0200 |
wenzelm |
basic setup of Isabelle setup tool --- pure Java, no dependencies;
|
changeset |
files
|
| Tue, 11 May 2021 21:21:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 11 May 2021 20:19:07 +0200 |
wenzelm |
guess package more directly;
|
changeset |
files
|
| Tue, 11 May 2021 18:56:33 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 11 May 2021 15:50:19 +0100 |
paulson |
Just one lemma
|
changeset |
files
|
| Tue, 11 May 2021 16:55:42 +0200 |
wenzelm |
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
|
changeset |
files
|
| Tue, 11 May 2021 16:30:24 +0200 |
wenzelm |
clarified platforms;
|
changeset |
files
|
| Tue, 11 May 2021 14:04:36 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 11 May 2021 14:03:39 +0200 |
wenzelm |
proper jEdit.props (amending ff716ecb0805);
|
changeset |
files
|
| Tue, 11 May 2021 13:45:09 +0200 |
wenzelm |
update to gmp-6.2.1, with support for arm64-darwin;
|
changeset |
files
|
| Tue, 11 May 2021 13:06:36 +0200 |
wenzelm |
clarified platforms;
|
changeset |
files
|
| Tue, 11 May 2021 12:21:39 +0200 |
wenzelm |
clarified options: implicitly support both x86_64 and arm64;
|
changeset |
files
|
| Tue, 11 May 2021 11:17:27 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Mon, 10 May 2021 19:46:01 +0000 |
haftmann |
centralized more lemmas
|
changeset |
files
|
| Mon, 10 May 2021 19:45:54 +0000 |
haftmann |
avoid Fun.swap
|
changeset |
files
|
| Mon, 10 May 2021 19:45:51 +0000 |
haftmann |
guide is out of focus
|
changeset |
files
|
| Mon, 10 May 2021 22:32:02 +0200 |
wenzelm |
proper build for fresh target directory (amending d9823224fcfe);
|
changeset |
files
|
| Mon, 10 May 2021 22:18:12 +0200 |
wenzelm |
put more resources into jedit_build component;
|
changeset |
files
|
| Mon, 10 May 2021 20:09:47 +0200 |
wenzelm |
more brackets (see f6b453449cc6);
|
changeset |
files
|
| Mon, 10 May 2021 18:31:18 +0200 |
wenzelm |
more brackets;
|
changeset |
files
|
| Mon, 10 May 2021 17:15:37 +0200 |
wenzelm |
proper settings variable, amending 6e85281177df;
|
changeset |
files
|
| Mon, 10 May 2021 16:26:15 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 10 May 2021 16:14:34 +0200 |
wenzelm |
tuned proofs --- avoid z3, which is absent on arm64-linux;
|
changeset |
files
|
| Mon, 10 May 2021 14:28:37 +0200 |
wenzelm |
proper condition: z3 could be absent, e.g. on arm64-linux;
|
changeset |
files
|
| Mon, 10 May 2021 12:23:30 +0200 |
wenzelm |
build auxiliary jEdit component in Isabelle/Scala;
|
changeset |
files
|
| Sat, 08 May 2021 13:06:30 +0200 |
wenzelm |
separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);
|
changeset |
files
|
| Sat, 08 May 2021 00:31:51 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Fri, 07 May 2021 23:56:18 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 07 May 2021 21:03:20 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 09 May 2021 05:48:50 +0000 |
haftmann |
more elementary swap
|
changeset |
files
|
| Fri, 07 May 2021 16:49:08 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Fri, 07 May 2021 16:45:49 +0200 |
wenzelm |
misc updates and clarification;
|
changeset |
files
|
| Fri, 07 May 2021 16:44:39 +0200 |
wenzelm |
clarified file name;
|
changeset |
files
|
| Fri, 07 May 2021 13:37:48 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 07 May 2021 13:34:01 +0200 |
wenzelm |
updated to polyml-5.8.2 (official release);
|
changeset |
files
|
| Fri, 07 May 2021 13:17:29 +0200 |
wenzelm |
clarified default_platform_families (again);
|
changeset |
files
|
| Fri, 07 May 2021 13:16:50 +0200 |
wenzelm |
proper option for linux_arm;
|
changeset |
files
|
| Fri, 07 May 2021 12:43:03 +0200 |
wenzelm |
proper "$?";
|
changeset |
files
|
| Thu, 06 May 2021 23:28:30 +0200 |
wenzelm |
proper jvm_platform, notably for org.sqlite.lib.path;
|
changeset |
files
|
| Thu, 06 May 2021 23:20:02 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 06 May 2021 23:09:19 +0200 |
wenzelm |
support for platform family "linux_arm";
|
changeset |
files
|
| Thu, 06 May 2021 22:13:30 +0200 |
wenzelm |
clarified purge;
|
changeset |
files
|
| Thu, 06 May 2021 20:54:34 +0200 |
wenzelm |
removed junk;
|
changeset |
files
|
| Thu, 06 May 2021 20:43:12 +0200 |
wenzelm |
support local build_heaps;
|
changeset |
files
|
| Wed, 05 May 2021 21:14:38 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 05 May 2021 20:41:40 +0200 |
wenzelm |
tuned --- rename = dist_name is sufficient;
|
changeset |
files
|
| Wed, 05 May 2021 20:37:49 +0200 |
wenzelm |
proper dist_name;
|
changeset |
files
|
| Wed, 05 May 2021 14:17:25 +0200 |
wenzelm |
clarified option -P: allow empty argument;
|
changeset |
files
|
| Wed, 05 May 2021 14:07:25 +0200 |
wenzelm |
support for existing release archive;
|
changeset |
files
|
| Wed, 05 May 2021 13:30:11 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 05 May 2021 13:27:30 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 04 May 2021 20:40:09 +0200 |
wenzelm |
more website content;
|
changeset |
files
|
| Tue, 04 May 2021 20:02:08 +0200 |
wenzelm |
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
|
changeset |
files
|
| Tue, 04 May 2021 12:54:54 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 05 May 2021 16:09:02 +0000 |
haftmann |
tuned theory structure
|
changeset |
files
|
| Wed, 05 May 2021 16:09:02 +0000 |
haftmann |
more appropriate location
|
changeset |
files
|
| Tue, 04 May 2021 17:57:16 +0000 |
haftmann |
collected lemmas on permutations
|
changeset |
files
|
| Mon, 03 May 2021 21:49:30 +0100 |
paulson |
A nice cardinality lemma
|
changeset |
files
|
| Mon, 03 May 2021 19:06:33 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 02 May 2021 21:46:59 +0200 |
wenzelm |
more robust indentation: proper line context after insert;
|
changeset |
files
|
| Sun, 02 May 2021 20:51:21 +0200 |
wenzelm |
more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();
|
changeset |
files
|
| Sun, 02 May 2021 17:38:49 +0200 |
wenzelm |
support nested cases;
|
changeset |
files
|
| Sun, 02 May 2021 15:56:58 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 02 May 2021 15:22:19 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 02 May 2021 14:07:19 +0200 |
wenzelm |
early definition of ML antiquotations;
|
changeset |
files
|
| Sat, 01 May 2021 11:54:09 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 29 Apr 2021 22:39:33 +0200 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Thu, 29 Apr 2021 15:49:04 +0200 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Wed, 28 Apr 2021 23:20:05 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 28 Apr 2021 14:03:26 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 28 Apr 2021 13:03:09 +0200 |
wenzelm |
clarified command-line, following other build_XYZ tools;
|
changeset |
files
|
| Wed, 28 Apr 2021 12:24:39 +0200 |
wenzelm |
more recent OCaml and GHC stack: better support for Apple Silicon;
|
changeset |
files
|
| Sun, 25 Apr 2021 22:33:53 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 25 Apr 2021 22:33:15 +0200 |
wenzelm |
avoid "exec" to change the winpid;
|
changeset |
files
|
| Sun, 25 Apr 2021 21:12:59 +0200 |
wenzelm |
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
|
changeset |
files
|
| Thu, 22 Apr 2021 23:40:22 +0200 |
wenzelm |
fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
|
changeset |
files
|
| Thu, 22 Apr 2021 23:03:58 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 22 Apr 2021 22:55:41 +0200 |
wenzelm |
rebuild executable for x86_64-darwin;
|
changeset |
files
|
| Thu, 22 Apr 2021 22:07:05 +0200 |
wenzelm |
clarified command-line;
|
changeset |
files
|
| Thu, 22 Apr 2021 22:04:54 +0200 |
wenzelm |
update Linux base-line;
|
changeset |
files
|
| Thu, 22 Apr 2021 11:12:03 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 22 Apr 2021 10:55:31 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 22 Apr 2021 10:11:11 +0200 |
wenzelm |
simplified typesetting of \<guillemotleft>...\<guillemotright>;
|
changeset |
files
|
| Fri, 23 Apr 2021 09:50:14 +0000 |
haftmann |
collecting more lemmas concerning multisets
|
changeset |
files
|
| Tue, 20 Apr 2021 22:53:24 +0200 |
wenzelm |
proper use of antiquotations;
|
changeset |
files
|
| Mon, 19 Apr 2021 21:57:52 +0200 |
wenzelm |
more documentation on "Conversions";
|
changeset |
files
|
| Mon, 19 Apr 2021 15:55:14 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Sat, 17 Apr 2021 19:47:08 +0200 |
wenzelm |
updated example;
|
changeset |
files
|
| Sat, 17 Apr 2021 19:45:12 +0200 |
wenzelm |
clarified options (again);
|
changeset |
files
|
| Sat, 17 Apr 2021 19:37:42 +0200 |
wenzelm |
more options: update ISABELLE_IDENTIFIER;
|
changeset |
files
|
| Fri, 16 Apr 2021 23:35:20 +0200 |
wenzelm |
clarified conditional ML;
|
changeset |
files
|
| Fri, 16 Apr 2021 23:16:00 +0200 |
wenzelm |
support for conditional ML text;
|
changeset |
files
|
| Fri, 16 Apr 2021 21:54:08 +0200 |
wenzelm |
updated example;
|
changeset |
files
|
| Fri, 16 Apr 2021 21:50:47 +0200 |
wenzelm |
clarified options;
|
changeset |
files
|
| Thu, 15 Apr 2021 19:45:43 +0000 |
haftmann |
proper context variable handling when stripping leadings quantifiers from test goals
|
changeset |
files
|
| Wed, 14 Apr 2021 21:15:24 +0200 |
wenzelm |
proper etc/ISABELLE_ID from archive (amending 4cba4e250c28);
|
changeset |
files
|
| Wed, 14 Apr 2021 20:53:28 +0200 |
wenzelm |
eliminated perl: prefer elementary GNU printenv;
|
changeset |
files
|
| Wed, 14 Apr 2021 14:36:13 +0200 |
wenzelm |
more robust bootstrap of components;
|
changeset |
files
|
| Wed, 14 Apr 2021 14:28:30 +0200 |
wenzelm |
more self-contained support for macOS;
|
changeset |
files
|
| Tue, 13 Apr 2021 16:19:43 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Tue, 13 Apr 2021 11:44:47 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 12 Apr 2021 22:57:39 +0200 |
wenzelm |
support for base64 via Isabelle/Scala/ML;
|
changeset |
files
|
| Mon, 12 Apr 2021 22:45:38 +0200 |
wenzelm |
compile;
|
changeset |
files
|
| Mon, 12 Apr 2021 22:41:51 +0200 |
wenzelm |
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
|
changeset |
files
|
| Mon, 12 Apr 2021 22:36:13 +0200 |
wenzelm |
clarified signature (again);
|
changeset |
files
|
| Mon, 12 Apr 2021 22:26:30 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 12 Apr 2021 22:26:09 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 12 Apr 2021 22:18:37 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Mon, 12 Apr 2021 22:17:48 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Mon, 12 Apr 2021 22:16:31 +0200 |
wenzelm |
clarified signature: more structured arguments, notably for remote provers;
|
changeset |
files
|
| Mon, 12 Apr 2021 21:48:04 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 12 Apr 2021 18:29:34 +0200 |
wenzelm |
clarified signature: avoid tmp file;
|
changeset |
files
|
| Mon, 12 Apr 2021 18:10:13 +0200 |
wenzelm |
clarified signature for Scala functions;
|
changeset |
files
|
| Mon, 12 Apr 2021 15:00:03 +0200 |
wenzelm |
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
|
changeset |
files
|
| Mon, 12 Apr 2021 14:14:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 12 Apr 2021 12:32:09 +0200 |
wenzelm |
clarified cache;
|
changeset |
files
|
| Mon, 12 Apr 2021 12:16:49 +0200 |
wenzelm |
clarified signature: Bytes extends CharSequence already (see d201996f72a8);
|
changeset |
files
|
| Mon, 12 Apr 2021 11:45:16 +0200 |
wenzelm |
clarified exceptions;
|
changeset |
files
|
| Sun, 11 Apr 2021 22:47:55 +0200 |
wenzelm |
more uniform use of Byte_Message;
|
changeset |
files
|
| Sun, 11 Apr 2021 21:32:09 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 11 Apr 2021 21:23:51 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 10 Apr 2021 21:50:59 +0200 |
wenzelm |
more robust treatment of empty markup: it allows to produce formal chunks;
|
changeset |
files
|
| Sun, 11 Apr 2021 07:35:24 +0000 |
haftmann |
collected combinatorial material
|
changeset |
files
|
| Sat, 10 Apr 2021 20:22:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 10 Apr 2021 19:45:51 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 10 Apr 2021 14:56:03 +0200 |
wenzelm |
more documentation;
|
changeset |
files
|
| Sat, 10 Apr 2021 14:55:50 +0200 |
wenzelm |
proper treatment of nested antiquotations;
|
changeset |
files
|
| Fri, 09 Apr 2021 22:06:59 +0200 |
wenzelm |
support for ML special forms: modified evaluation similar to Scheme;
|
changeset |
files
|
| Fri, 09 Apr 2021 21:07:11 +0200 |
wenzelm |
clarified signature: more detailed token positions for antiquotations;
|
changeset |
files
|
| Thu, 08 Apr 2021 20:52:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 08 Apr 2021 16:43:35 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 08 Apr 2021 12:38:18 +0000 |
haftmann |
confluent preprocessing for floats in presence of target language numerals
|
changeset |
files
|
| Wed, 07 Apr 2021 15:46:06 +0000 |
haftmann |
subclass relation
|
changeset |
files
|
| Wed, 07 Apr 2021 22:32:43 +0200 |
wenzelm |
some tinkering with npm versions;
|
changeset |
files
|
| Wed, 07 Apr 2021 22:28:41 +0200 |
wenzelm |
some tinkering with npm versions;
|
changeset |
files
|
| Wed, 07 Apr 2021 18:13:02 +0200 |
wenzelm |
back to post-release mode;
|
changeset |
files
|
| Wed, 07 Apr 2021 18:05:48 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 07 Apr 2021 18:05:14 +0200 |
wenzelm |
auto-update due to "isabelle build_vscode";
|
changeset |
files
|
| Wed, 07 Apr 2021 18:04:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 07 Apr 2021 18:04:30 +0200 |
wenzelm |
tuned --- following hints by IntelliJ IDEA;
|
changeset |
files
|
| Wed, 07 Apr 2021 11:05:00 +0200 |
Manuel Eberl |
fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes)
|
changeset |
files
|
| Wed, 07 Apr 2021 12:28:19 +0000 |
haftmann |
simplified definition
|
changeset |
files
|
| Tue, 06 Apr 2021 18:12:20 +0000 |
haftmann |
new lemmas
|
changeset |
files
|
| Mon, 05 Apr 2021 22:46:41 +0200 |
wenzelm |
discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove";
|
changeset |
files
|
| Mon, 05 Apr 2021 22:45:01 +0200 |
wenzelm |
following recent Phabricator update, after 2021 Week 13 (Late March);
|
changeset |
files
|
| Fri, 02 Apr 2021 12:24:35 +0100 |
paulson |
merged
|
changeset |
files
|
| Fri, 02 Apr 2021 12:24:29 +0100 |
paulson |
Cosmetic: no !! in the lemma statement
|
changeset |
files
|
| Thu, 01 Apr 2021 19:14:43 +0200 |
wenzelm |
clarified README;
|
changeset |
files
|
| Thu, 01 Apr 2021 19:07:06 +0200 |
wenzelm |
more standard header, with utf-8 encoding;
|
changeset |
files
|
| Thu, 01 Apr 2021 19:01:19 +0200 |
wenzelm |
clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;
|
changeset |
files
|
| Thu, 01 Apr 2021 07:35:03 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 31 Mar 2021 18:18:03 +0200 |
nipkow |
new automatic order prover: stateless, complete, verified
|
changeset |
files
|
| Wed, 31 Mar 2021 23:45:16 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 31 Mar 2021 23:13:13 +0200 |
wenzelm |
clarified: follow "isabelle version -t";
|
changeset |
files
|
| Wed, 31 Mar 2021 22:58:17 +0200 |
wenzelm |
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
|
changeset |
files
|
| Wed, 31 Mar 2021 22:10:56 +0200 |
wenzelm |
tuned signature -- more explicit types;
|
changeset |
files
|
| Wed, 31 Mar 2021 21:44:29 +0200 |
wenzelm |
more robust and uniform ISABELLE_TAGS;
|
changeset |
files
|
| Wed, 31 Mar 2021 18:12:46 +0200 |
wenzelm |
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
|
changeset |
files
|
| Wed, 31 Mar 2021 17:15:54 +0200 |
wenzelm |
simplified release status (again), in contrast to a43898f76ae9;
|
changeset |
files
|
| Wed, 31 Mar 2021 12:02:52 +0200 |
wenzelm |
more uniform HTTP resources;
|
changeset |
files
|
| Wed, 31 Mar 2021 11:24:46 +0200 |
wenzelm |
clarified (again): local tip could be actually more recent;
|
changeset |
files
|
| Wed, 31 Mar 2021 11:21:08 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 31 Mar 2021 11:17:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 31 Mar 2021 11:05:40 +0200 |
wenzelm |
clarified name;
|
changeset |
files
|
| Wed, 31 Mar 2021 10:57:18 +0200 |
wenzelm |
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
|
changeset |
files
|
| Tue, 30 Mar 2021 12:32:24 +0200 |
wenzelm |
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
|
changeset |
files
|
| Tue, 30 Mar 2021 09:42:25 +0200 |
nipkow |
updated to latest latex due to new mechanism for dealing with bold ccfonts
|
changeset |
files
|
| Mon, 29 Mar 2021 12:26:13 +0100 |
paulson |
removal of needless hypothesis in hd_rev and last_rev
|
changeset |
files
|
| Sun, 28 Mar 2021 12:21:37 +0200 |
wenzelm |
more robust;
|
changeset |
files
|
| Sun, 28 Mar 2021 12:10:14 +0200 |
wenzelm |
clarified message;
|
changeset |
files
|
| Sun, 28 Mar 2021 12:08:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 28 Mar 2021 12:07:46 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sun, 28 Mar 2021 12:02:20 +0200 |
wenzelm |
proper export;
|
changeset |
files
|
| Sun, 28 Mar 2021 11:59:30 +0200 |
wenzelm |
more options: build is part of default setup;
|
changeset |
files
|
| Sun, 28 Mar 2021 11:45:00 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sun, 28 Mar 2021 11:39:53 +0200 |
wenzelm |
more options;
|
changeset |
files
|
| Sun, 28 Mar 2021 11:35:08 +0200 |
wenzelm |
proper Admin script, outside the settings environment;
|
changeset |
files
|
| Sun, 28 Mar 2021 11:33:30 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 27 Mar 2021 23:03:57 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 27 Mar 2021 22:59:12 +0100 |
wenzelm |
clarified;
|
changeset |
files
|
| Sat, 27 Mar 2021 22:48:59 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sat, 27 Mar 2021 22:48:15 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sat, 27 Mar 2021 22:36:45 +0100 |
wenzelm |
more accurate settings after update of current version;
|
changeset |
files
|
| Sat, 27 Mar 2021 22:26:13 +0100 |
wenzelm |
clarified messages;
|
changeset |
files
|
| Sat, 27 Mar 2021 22:19:56 +0100 |
wenzelm |
more robust: lest hg work out remote tip;
|
changeset |
files
|
| Sat, 27 Mar 2021 22:09:49 +0100 |
wenzelm |
more options;
|
changeset |
files
|
| Sat, 27 Mar 2021 21:27:27 +0100 |
wenzelm |
clarified treatment of multiple versions: last one counts;
|
changeset |
files
|
| Sat, 27 Mar 2021 20:53:11 +0100 |
wenzelm |
more robust;
|
changeset |
files
|
| Sat, 27 Mar 2021 20:39:14 +0100 |
wenzelm |
more robust: explicit repository root;
|
changeset |
files
|
| Sat, 27 Mar 2021 20:37:49 +0100 |
wenzelm |
more robust;
|
changeset |
files
|
| Sat, 27 Mar 2021 20:24:04 +0100 |
wenzelm |
more convenient repository setup;
|
changeset |
files
|
| Sat, 27 Mar 2021 19:46:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 27 Mar 2021 19:44:36 +0100 |
wenzelm |
more robust invocation of hg;
|
changeset |
files
|
| Sat, 27 Mar 2021 19:26:34 +0100 |
wenzelm |
more robust: idempotent;
|
changeset |
files
|
| Sat, 27 Mar 2021 18:15:19 +0100 |
wenzelm |
more robust invocation of hg;
|
changeset |
files
|
| Sat, 27 Mar 2021 18:03:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 27 Mar 2021 18:01:41 +0100 |
wenzelm |
clarified output;
|
changeset |
files
|
| Sat, 27 Mar 2021 17:13:15 +0100 |
wenzelm |
support repository archives (without full .hg directory);
|
changeset |
files
|
| Sat, 27 Mar 2021 17:05:36 +0100 |
wenzelm |
more robust invocation of hg;
|
changeset |
files
|
| Sat, 27 Mar 2021 15:56:49 +0100 |
wenzelm |
record official releases that follow a certain structure, with public access via https://isabelle.sketis.net/repos/isabelle/raw-file/tip/Admin/Release/official (NB: Isabelle2013-1 had to be retracted);
|
changeset |
files
|
| Thu, 25 Mar 2021 08:52:15 +0000 |
haftmann |
dedicated session for combinatorial material
|
changeset |
files
|
| Wed, 24 Mar 2021 21:17:19 +0100 |
wenzelm |
support for Java Chromium Embedded Framework (JCEF): still somewhat fragile;
|
changeset |
files
|
| Tue, 23 Mar 2021 19:47:15 +0100 |
wenzelm |
enforce full build;
|
changeset |
files
|
| Tue, 23 Mar 2021 13:27:15 +0100 |
wenzelm |
turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont;
|
changeset |
files
|
| Tue, 23 Mar 2021 13:13:31 +0100 |
wenzelm |
discontinue fragile check in LaTeX, e.g. problems with toc entries;
|
changeset |
files
|
| Mon, 22 Mar 2021 21:24:25 +0000 |
paulson |
merged
|
changeset |
files
|
| Mon, 22 Mar 2021 12:18:43 +0000 |
paulson |
merged
|
changeset |
files
|
| Mon, 22 Mar 2021 12:18:35 +0000 |
paulson |
type class relaxation
|
changeset |
files
|
| Mon, 22 Mar 2021 17:33:08 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Mon, 22 Mar 2021 17:28:07 +0100 |
wenzelm |
clarified group (but hard to tell);
|
changeset |
files
|
| Mon, 22 Mar 2021 17:24:42 +0100 |
wenzelm |
more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
|
changeset |
files
|
| Mon, 22 Mar 2021 10:49:51 +0000 |
haftmann |
more lemmas
|
changeset |
files
|
| Mon, 22 Mar 2021 00:07:55 +0100 |
wenzelm |
clarified package name (actually both pxfonts and txfonts exist and have this font);
|
changeset |
files
|
| Sun, 21 Mar 2021 23:56:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Mar 2021 23:24:20 +0100 |
wenzelm |
prefer isabelle bbbfont;
|
changeset |
files
|
| Sun, 21 Mar 2021 23:16:34 +0100 |
wenzelm |
enforce full build;
|
changeset |
files
|
| Sun, 21 Mar 2021 23:15:55 +0100 |
wenzelm |
clarified symbol names, notably relevant for Z_Notation;
|
changeset |
files
|
| Sun, 21 Mar 2021 23:05:17 +0100 |
wenzelm |
update README (actually after update of component);
|
changeset |
files
|
| Sun, 21 Mar 2021 23:03:31 +0100 |
wenzelm |
high-quality blackboard-bold fonts from "txmia" (package "txfonts");
|
changeset |
files
|
| Fri, 19 Mar 2021 23:37:12 +0100 |
wenzelm |
publish component;
|
changeset |
files
|
| Fri, 19 Mar 2021 23:35:37 +0100 |
wenzelm |
further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
|
changeset |
files
|
| Fri, 19 Mar 2021 13:44:33 +0100 |
wenzelm |
clarified \<Zcomp> (small) vs. \<Zsemi> (big);
|
changeset |
files
|
| Fri, 19 Mar 2021 13:22:12 +0100 |
wenzelm |
more CONTRIBUTORS;
|
changeset |
files
|
| Fri, 19 Mar 2021 12:35:55 +0100 |
wenzelm |
more Z_Notation symbols, as proposed by Simon Foster;
|
changeset |
files
|
| Thu, 18 Mar 2021 21:49:19 +0100 |
wenzelm |
more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus";
|
changeset |
files
|
| Thu, 18 Mar 2021 21:36:19 +0100 |
wenzelm |
clarified order for GUI panel;
|
changeset |
files
|
| Thu, 18 Mar 2021 06:37:24 +0000 |
haftmann |
prefer more direct interpretation
|
changeset |
files
|
| Thu, 18 Mar 2021 13:03:29 +0100 |
wenzelm |
more Z_Notation symbols, as proposed by Simon Foster;
|
changeset |
files
|
| Thu, 18 Mar 2021 12:53:05 +0100 |
wenzelm |
more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt;
|
changeset |
files
|
| Thu, 18 Mar 2021 12:46:25 +0100 |
wenzelm |
clarified order for presentation in isar-ref (Appendix B);
|
changeset |
files
|
| Thu, 18 Mar 2021 12:41:17 +0100 |
wenzelm |
prefer explicit \<Zproject> (with its own Unicode codepoint);
|
changeset |
files
|
| Wed, 17 Mar 2021 22:24:57 +0100 |
wenzelm |
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
|
changeset |
files
|
| Tue, 16 Mar 2021 23:30:51 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Tue, 16 Mar 2021 22:13:04 +0100 |
wenzelm |
proper directory of settings file;
|
changeset |
files
|
| Tue, 16 Mar 2021 08:42:21 +0100 |
nipkow |
tuned lemma
|
changeset |
files
|
| Mon, 15 Mar 2021 22:58:20 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Mon, 15 Mar 2021 11:50:58 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 15 Mar 2021 11:43:56 +0100 |
wenzelm |
tuned signature (again);
|
changeset |
files
|
| Sun, 14 Mar 2021 22:55:52 +0100 |
wenzelm |
tuned --- following hints by IntelliJ;
|
changeset |
files
|
| Sun, 14 Mar 2021 22:34:41 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sun, 14 Mar 2021 21:41:28 +0100 |
wenzelm |
proper shell quote;
|
changeset |
files
|
| Sun, 14 Mar 2021 21:02:34 +0100 |
wenzelm |
removed spurious references to perl / libwww-perl;
|
changeset |
files
|
| Sun, 14 Mar 2021 20:29:26 +0100 |
wenzelm |
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
|
changeset |
files
|
| Sun, 14 Mar 2021 18:32:11 +0100 |
wenzelm |
clarified signature: refer to file name instead of file content;
|
changeset |
files
|
| Sun, 14 Mar 2021 18:27:55 +0100 |
wenzelm |
compile;
|
changeset |
files
|
| Sun, 14 Mar 2021 16:50:11 +0100 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Sun, 14 Mar 2021 15:28:44 +0100 |
wenzelm |
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
|
changeset |
files
|
| Sun, 14 Mar 2021 13:21:59 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 14 Mar 2021 13:09:17 +0100 |
wenzelm |
elapsed time to download content (and for the server to provide content);
|
changeset |
files
|
| Sat, 13 Mar 2021 19:29:45 +0100 |
wenzelm |
more direct elapsed run_time via bash_process wrapper (via Scala and C);
|
changeset |
files
|
| Sat, 13 Mar 2021 15:39:48 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 13 Mar 2021 15:14:46 +0100 |
wenzelm |
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
|
changeset |
files
|
| Sat, 13 Mar 2021 14:55:27 +0100 |
wenzelm |
clarified signature: let Sledgehammer handle SystemOnTPTP comments;
|
changeset |
files
|
| Sat, 13 Mar 2021 14:27:34 +0100 |
wenzelm |
clarified signature: url may change dynamically and is part of result;
|
changeset |
files
|
| Sat, 13 Mar 2021 14:27:07 +0100 |
wenzelm |
clarified error;
|
changeset |
files
|
| Sat, 13 Mar 2021 14:08:25 +0100 |
wenzelm |
support timeout, similar to perl LWP::UserAgent;
|
changeset |
files
|
| Sat, 13 Mar 2021 13:44:42 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 13 Mar 2021 12:45:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 13 Mar 2021 12:36:24 +0100 |
wenzelm |
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
|
changeset |
files
|
| Fri, 12 Mar 2021 23:30:35 +0100 |
wenzelm |
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
|
changeset |
files
|
| Fri, 12 Mar 2021 23:00:01 +0100 |
wenzelm |
clarified HTTP.Content: support encoding;
|
changeset |
files
|
| Fri, 12 Mar 2021 19:46:37 +0100 |
wenzelm |
clarified signature: more explicit HTTP operations;
|
changeset |
files
|
| Fri, 12 Mar 2021 19:43:49 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 12 Mar 2021 19:42:18 +0100 |
wenzelm |
more robust;
|
changeset |
files
|
| Thu, 11 Mar 2021 20:30:56 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 11 Mar 2021 12:16:17 +0100 |
wenzelm |
clarified components;
|
changeset |
files
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
changeset |
files
|
| Thu, 11 Mar 2021 07:05:29 +0000 |
haftmann |
lemma
|
changeset |
files
|
| Thu, 11 Mar 2021 11:22:25 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Mar 2021 10:25:04 +0100 |
traytel |
another example for lift_bnf for quotients
|
changeset |
files
|
| Wed, 10 Mar 2021 21:55:28 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Mar 2021 20:09:26 +0100 |
wenzelm |
proper \usepackage[T1]{fontenc};
|
changeset |
files
|
| Wed, 10 Mar 2021 19:03:24 +0100 |
wenzelm |
more robust init: avoid spilling opam artifacts;
|
changeset |
files
|
| Tue, 09 Mar 2021 21:11:05 +0100 |
wenzelm |
proper type-setting of cartouches (requires T1);
|
changeset |
files
|
| Tue, 09 Mar 2021 20:00:44 +0100 |
wenzelm |
provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04;
|
changeset |
files
|
| Tue, 09 Mar 2021 18:52:24 +0100 |
wenzelm |
more robust;
|
changeset |
files
|
| Tue, 09 Mar 2021 18:44:43 +0100 |
wenzelm |
removed unused latex packages;
|
changeset |
files
|
| Tue, 09 Mar 2021 17:31:51 +0100 |
wenzelm |
obsolete (see 0c837beeb5e7);
|
changeset |
files
|
| Tue, 09 Mar 2021 17:15:21 +0100 |
wenzelm |
proper Isabelle/Scala tool --- avoid perl;
|
changeset |
files
|
| Tue, 09 Mar 2021 14:20:27 +0100 |
traytel |
generalized confluence-based subdistributivity theorem for quotients;
|
changeset |
files
|
| Tue, 09 Mar 2021 11:50:21 +0100 |
desharna |
Backed out changeset 3fdb94d87e0e
|
changeset |
files
|
| Tue, 09 Mar 2021 11:50:11 +0100 |
desharna |
Backed out changeset b867b436f372
|
changeset |
files
|
| Sun, 07 Mar 2021 08:26:02 +0100 |
haftmann |
reduced dependencies on List_Permutation
|
changeset |
files
|