Wed, 12 May 2021 17:05:29 +0000 explicit type class operations for type-specific implementations default tip
haftmann [Wed, 12 May 2021 17:05:29 +0000] rev 73682
explicit type class operations for type-specific implementations
Wed, 12 May 2021 17:05:28 +0000 obsolete
haftmann [Wed, 12 May 2021 17:05:28 +0000] rev 73681
obsolete
Wed, 12 May 2021 09:31:18 +0200 added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran
desharna [Wed, 12 May 2021 09:31:18 +0200] rev 73680
added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran
Wed, 12 May 2021 06:35:16 +0200 merged
nipkow [Wed, 12 May 2021 06:35:16 +0200] rev 73679
merged
Tue, 11 May 2021 22:40:59 +0200 generalized type
nipkow [Tue, 11 May 2021 22:40:59 +0200] rev 73678
generalized type
Tue, 11 May 2021 21:57:43 +0200 basic setup of Isabelle setup tool --- pure Java, no dependencies;
wenzelm [Tue, 11 May 2021 21:57:43 +0200] rev 73677
basic setup of Isabelle setup tool --- pure Java, no dependencies;
Tue, 11 May 2021 21:21:01 +0200 merged
wenzelm [Tue, 11 May 2021 21:21:01 +0200] rev 73676
merged
Tue, 11 May 2021 20:19:07 +0200 guess package more directly;
wenzelm [Tue, 11 May 2021 20:19:07 +0200] rev 73675
guess package more directly;
Tue, 11 May 2021 18:56:33 +0100 merged
paulson [Tue, 11 May 2021 18:56:33 +0100] rev 73674
merged
Tue, 11 May 2021 15:50:19 +0100 Just one lemma
paulson <lp15@cam.ac.uk> [Tue, 11 May 2021 15:50:19 +0100] rev 73673
Just one lemma
Tue, 11 May 2021 16:55:42 +0200 proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm [Tue, 11 May 2021 16:55:42 +0200] rev 73672
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
Tue, 11 May 2021 16:30:24 +0200 clarified platforms;
wenzelm [Tue, 11 May 2021 16:30:24 +0200] rev 73671
clarified platforms;
Tue, 11 May 2021 14:04:36 +0200 merged
wenzelm [Tue, 11 May 2021 14:04:36 +0200] rev 73670
merged
Tue, 11 May 2021 14:03:39 +0200 proper jEdit.props (amending ff716ecb0805);
wenzelm [Tue, 11 May 2021 14:03:39 +0200] rev 73669
proper jEdit.props (amending ff716ecb0805);
Tue, 11 May 2021 13:45:09 +0200 update to gmp-6.2.1, with support for arm64-darwin;
wenzelm [Tue, 11 May 2021 13:45:09 +0200] rev 73668
update to gmp-6.2.1, with support for arm64-darwin;
Tue, 11 May 2021 13:06:36 +0200 clarified platforms;
wenzelm [Tue, 11 May 2021 13:06:36 +0200] rev 73667
clarified platforms;
Tue, 11 May 2021 12:21:39 +0200 clarified options: implicitly support both x86_64 and arm64;
wenzelm [Tue, 11 May 2021 12:21:39 +0200] rev 73666
clarified options: implicitly support both x86_64 and arm64;
Tue, 11 May 2021 11:17:27 +0200 tuned whitespace;
wenzelm [Tue, 11 May 2021 11:17:27 +0200] rev 73665
tuned whitespace;
Mon, 10 May 2021 19:46:01 +0000 centralized more lemmas
haftmann [Mon, 10 May 2021 19:46:01 +0000] rev 73664
centralized more lemmas
Mon, 10 May 2021 19:45:54 +0000 avoid Fun.swap
haftmann [Mon, 10 May 2021 19:45:54 +0000] rev 73663
avoid Fun.swap
Mon, 10 May 2021 19:45:51 +0000 guide is out of focus
haftmann [Mon, 10 May 2021 19:45:51 +0000] rev 73662
guide is out of focus
Mon, 10 May 2021 22:32:02 +0200 proper build for fresh target directory (amending d9823224fcfe);
wenzelm [Mon, 10 May 2021 22:32:02 +0200] rev 73661
proper build for fresh target directory (amending d9823224fcfe);
Mon, 10 May 2021 22:18:12 +0200 put more resources into jedit_build component;
wenzelm [Mon, 10 May 2021 22:18:12 +0200] rev 73660
put more resources into jedit_build component;
Mon, 10 May 2021 20:09:47 +0200 more brackets (see f6b453449cc6);
wenzelm [Mon, 10 May 2021 20:09:47 +0200] rev 73659
more brackets (see f6b453449cc6);
Mon, 10 May 2021 18:31:18 +0200 more brackets;
wenzelm [Mon, 10 May 2021 18:31:18 +0200] rev 73658
more brackets;
Mon, 10 May 2021 17:15:37 +0200 proper settings variable, amending 6e85281177df;
wenzelm [Mon, 10 May 2021 17:15:37 +0200] rev 73657
proper settings variable, amending 6e85281177df;
Mon, 10 May 2021 16:26:15 +0200 merged
wenzelm [Mon, 10 May 2021 16:26:15 +0200] rev 73656
merged
Mon, 10 May 2021 16:14:34 +0200 tuned proofs --- avoid z3, which is absent on arm64-linux;
wenzelm [Mon, 10 May 2021 16:14:34 +0200] rev 73655
tuned proofs --- avoid z3, which is absent on arm64-linux;
Mon, 10 May 2021 14:28:37 +0200 proper condition: z3 could be absent, e.g. on arm64-linux;
wenzelm [Mon, 10 May 2021 14:28:37 +0200] rev 73654
proper condition: z3 could be absent, e.g. on arm64-linux;
Mon, 10 May 2021 12:23:30 +0200 build auxiliary jEdit component in Isabelle/Scala;
wenzelm [Mon, 10 May 2021 12:23:30 +0200] rev 73653
build auxiliary jEdit component in Isabelle/Scala; clarified directory layout;
Sat, 08 May 2021 13:06:30 +0200 separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);
wenzelm [Sat, 08 May 2021 13:06:30 +0200] rev 73652
separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);
Sat, 08 May 2021 00:31:51 +0200 tuned message;
wenzelm [Sat, 08 May 2021 00:31:51 +0200] rev 73651
tuned message;
Fri, 07 May 2021 23:56:18 +0200 clarified signature;
wenzelm [Fri, 07 May 2021 23:56:18 +0200] rev 73650
clarified signature;
Fri, 07 May 2021 21:03:20 +0200 tuned signature;
wenzelm [Fri, 07 May 2021 21:03:20 +0200] rev 73649
tuned signature;
Sun, 09 May 2021 05:48:50 +0000 more elementary swap
haftmann [Sun, 09 May 2021 05:48:50 +0000] rev 73648
more elementary swap
Fri, 07 May 2021 16:49:08 +0200 tuned comments;
wenzelm [Fri, 07 May 2021 16:49:08 +0200] rev 73647
tuned comments;
Fri, 07 May 2021 16:45:49 +0200 misc updates and clarification;
wenzelm [Fri, 07 May 2021 16:45:49 +0200] rev 73646
misc updates and clarification;
Fri, 07 May 2021 16:44:39 +0200 clarified file name;
wenzelm [Fri, 07 May 2021 16:44:39 +0200] rev 73645
clarified file name;
Fri, 07 May 2021 13:37:48 +0200 merged
wenzelm [Fri, 07 May 2021 13:37:48 +0200] rev 73644
merged
Fri, 07 May 2021 13:34:01 +0200 updated to polyml-5.8.2 (official release);
wenzelm [Fri, 07 May 2021 13:34:01 +0200] rev 73643
updated to polyml-5.8.2 (official release);
Fri, 07 May 2021 13:17:29 +0200 clarified default_platform_families (again);
wenzelm [Fri, 07 May 2021 13:17:29 +0200] rev 73642
clarified default_platform_families (again);
Fri, 07 May 2021 13:16:50 +0200 proper option for linux_arm;
wenzelm [Fri, 07 May 2021 13:16:50 +0200] rev 73641
proper option for linux_arm;
Fri, 07 May 2021 12:43:03 +0200 proper "$?";
wenzelm [Fri, 07 May 2021 12:43:03 +0200] rev 73640
proper "$?";
Thu, 06 May 2021 23:28:30 +0200 proper jvm_platform, notably for org.sqlite.lib.path;
wenzelm [Thu, 06 May 2021 23:28:30 +0200] rev 73639
proper jvm_platform, notably for org.sqlite.lib.path;
Thu, 06 May 2021 23:20:02 +0200 tuned message;
wenzelm [Thu, 06 May 2021 23:20:02 +0200] rev 73638
tuned message;
Thu, 06 May 2021 23:09:19 +0200 support for platform family "linux_arm";
wenzelm [Thu, 06 May 2021 23:09:19 +0200] rev 73637
support for platform family "linux_arm";
Thu, 06 May 2021 22:13:30 +0200 clarified purge;
wenzelm [Thu, 06 May 2021 22:13:30 +0200] rev 73636
clarified purge;
Thu, 06 May 2021 20:54:34 +0200 removed junk;
wenzelm [Thu, 06 May 2021 20:54:34 +0200] rev 73635
removed junk;
Thu, 06 May 2021 20:43:12 +0200 support local build_heaps;
wenzelm [Thu, 06 May 2021 20:43:12 +0200] rev 73634
support local build_heaps; more robust build_release;
Wed, 05 May 2021 21:14:38 +0200 merged
wenzelm [Wed, 05 May 2021 21:14:38 +0200] rev 73633
merged
Wed, 05 May 2021 20:41:40 +0200 tuned --- rename = dist_name is sufficient;
wenzelm [Wed, 05 May 2021 20:41:40 +0200] rev 73632
tuned --- rename = dist_name is sufficient;
Wed, 05 May 2021 20:37:49 +0200 proper dist_name;
wenzelm [Wed, 05 May 2021 20:37:49 +0200] rev 73631
proper dist_name;
Wed, 05 May 2021 14:17:25 +0200 clarified option -P: allow empty argument;
wenzelm [Wed, 05 May 2021 14:17:25 +0200] rev 73630
clarified option -P: allow empty argument;
Wed, 05 May 2021 14:07:25 +0200 support for existing release archive;
wenzelm [Wed, 05 May 2021 14:07:25 +0200] rev 73629
support for existing release archive; misc tuning and clarification;
Wed, 05 May 2021 13:30:11 +0200 tuned signature;
wenzelm [Wed, 05 May 2021 13:30:11 +0200] rev 73628
tuned signature;
Wed, 05 May 2021 13:27:30 +0200 clarified signature;
wenzelm [Wed, 05 May 2021 13:27:30 +0200] rev 73627
clarified signature;
Tue, 04 May 2021 20:40:09 +0200 more website content;
wenzelm [Tue, 04 May 2021 20:40:09 +0200] rev 73626
more website content;
Tue, 04 May 2021 20:02:08 +0200 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm [Tue, 04 May 2021 20:02:08 +0200] rev 73625
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
Tue, 04 May 2021 12:54:54 +0200 tuned signature;
wenzelm [Tue, 04 May 2021 12:54:54 +0200] rev 73624
tuned signature;
Wed, 05 May 2021 16:09:02 +0000 tuned theory structure
haftmann [Wed, 05 May 2021 16:09:02 +0000] rev 73623
tuned theory structure
Wed, 05 May 2021 16:09:02 +0000 more appropriate location
haftmann [Wed, 05 May 2021 16:09:02 +0000] rev 73622
more appropriate location
Tue, 04 May 2021 17:57:16 +0000 collected lemmas on permutations
haftmann [Tue, 04 May 2021 17:57:16 +0000] rev 73621
collected lemmas on permutations
Mon, 03 May 2021 21:49:30 +0100 A nice cardinality lemma
paulson <lp15@cam.ac.uk> [Mon, 03 May 2021 21:49:30 +0100] rev 73620
A nice cardinality lemma
Mon, 03 May 2021 19:06:33 +0200 tuned
nipkow [Mon, 03 May 2021 19:06:33 +0200] rev 73619
tuned
Sun, 02 May 2021 21:46:59 +0200 more robust indentation: proper line context after insert;
wenzelm [Sun, 02 May 2021 21:46:59 +0200] rev 73618
more robust indentation: proper line context after insert;
Sun, 02 May 2021 20:51:21 +0200 more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();
wenzelm [Sun, 02 May 2021 20:51:21 +0200] rev 73617
more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();
Sun, 02 May 2021 17:38:49 +0200 support nested cases;
wenzelm [Sun, 02 May 2021 17:38:49 +0200] rev 73616
support nested cases;
Sun, 02 May 2021 15:56:58 +0200 tuned;
wenzelm [Sun, 02 May 2021 15:56:58 +0200] rev 73615
tuned;
Sun, 02 May 2021 15:22:19 +0200 tuned;
wenzelm [Sun, 02 May 2021 15:22:19 +0200] rev 73614
tuned;
Sun, 02 May 2021 14:07:19 +0200 early definition of ML antiquotations;
wenzelm [Sun, 02 May 2021 14:07:19 +0200] rev 73613
early definition of ML antiquotations;
Sat, 01 May 2021 11:54:09 +0200 tuned;
wenzelm [Sat, 01 May 2021 11:54:09 +0200] rev 73612
tuned;
Thu, 29 Apr 2021 22:39:33 +0200 clarified signature: more operations;
wenzelm [Thu, 29 Apr 2021 22:39:33 +0200] rev 73611
clarified signature: more operations;
Thu, 29 Apr 2021 15:49:04 +0200 clarified signature: more operations;
wenzelm [Thu, 29 Apr 2021 15:49:04 +0200] rev 73610
clarified signature: more operations;
Wed, 28 Apr 2021 23:20:05 +0200 clarified signature;
wenzelm [Wed, 28 Apr 2021 23:20:05 +0200] rev 73609
clarified signature;
Wed, 28 Apr 2021 14:03:26 +0200 tuned signature;
wenzelm [Wed, 28 Apr 2021 14:03:26 +0200] rev 73608
tuned signature;
Wed, 28 Apr 2021 13:03:09 +0200 clarified command-line, following other build_XYZ tools;
wenzelm [Wed, 28 Apr 2021 13:03:09 +0200] rev 73607
clarified command-line, following other build_XYZ tools;
Wed, 28 Apr 2021 12:24:39 +0200 more recent OCaml and GHC stack: better support for Apple Silicon;
wenzelm [Wed, 28 Apr 2021 12:24:39 +0200] rev 73606
more recent OCaml and GHC stack: better support for Apple Silicon;
Sun, 25 Apr 2021 22:33:53 +0200 merged
wenzelm [Sun, 25 Apr 2021 22:33:53 +0200] rev 73605
merged
Sun, 25 Apr 2021 22:33:15 +0200 avoid "exec" to change the winpid;
wenzelm [Sun, 25 Apr 2021 22:33:15 +0200] rev 73604
avoid "exec" to change the winpid;
Sun, 25 Apr 2021 21:12:59 +0200 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);
wenzelm [Sun, 25 Apr 2021 21:12:59 +0200] rev 73603
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);
Thu, 22 Apr 2021 23:40:22 +0200 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm [Thu, 22 Apr 2021 23:40:22 +0200] rev 73602
fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
Thu, 22 Apr 2021 23:03:58 +0200 clarified signature;
wenzelm [Thu, 22 Apr 2021 23:03:58 +0200] rev 73601
clarified signature;
Thu, 22 Apr 2021 22:55:41 +0200 rebuild executable for x86_64-darwin;
wenzelm [Thu, 22 Apr 2021 22:55:41 +0200] rev 73600
rebuild executable for x86_64-darwin;
Thu, 22 Apr 2021 22:07:05 +0200 clarified command-line;
wenzelm [Thu, 22 Apr 2021 22:07:05 +0200] rev 73599
clarified command-line;
Thu, 22 Apr 2021 22:04:54 +0200 update Linux base-line;
wenzelm [Thu, 22 Apr 2021 22:04:54 +0200] rev 73598
update Linux base-line;
Thu, 22 Apr 2021 11:12:03 +0200 tuned comments;
wenzelm [Thu, 22 Apr 2021 11:12:03 +0200] rev 73597
tuned comments;
Thu, 22 Apr 2021 10:55:31 +0200 tuned signature;
wenzelm [Thu, 22 Apr 2021 10:55:31 +0200] rev 73596
tuned signature;
Thu, 22 Apr 2021 10:11:11 +0200 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm [Thu, 22 Apr 2021 10:11:11 +0200] rev 73595
simplified typesetting of \<guillemotleft>...\<guillemotright>;
Fri, 23 Apr 2021 09:50:14 +0000 collecting more lemmas concerning multisets
haftmann [Fri, 23 Apr 2021 09:50:14 +0000] rev 73594
collecting more lemmas concerning multisets
Tue, 20 Apr 2021 22:53:24 +0200 proper use of antiquotations;
wenzelm [Tue, 20 Apr 2021 22:53:24 +0200] rev 73593
proper use of antiquotations;
Mon, 19 Apr 2021 21:57:52 +0200 more documentation on "Conversions";
wenzelm [Mon, 19 Apr 2021 21:57:52 +0200] rev 73592
more documentation on "Conversions";
Mon, 19 Apr 2021 15:55:14 +0200 tuned
nipkow [Mon, 19 Apr 2021 15:55:14 +0200] rev 73591
tuned
Sat, 17 Apr 2021 19:47:08 +0200 updated example;
wenzelm [Sat, 17 Apr 2021 19:47:08 +0200] rev 73590
updated example;
Sat, 17 Apr 2021 19:45:12 +0200 clarified options (again);
wenzelm [Sat, 17 Apr 2021 19:45:12 +0200] rev 73589
clarified options (again);
Sat, 17 Apr 2021 19:37:42 +0200 more options: update ISABELLE_IDENTIFIER;
wenzelm [Sat, 17 Apr 2021 19:37:42 +0200] rev 73588
more options: update ISABELLE_IDENTIFIER;
Fri, 16 Apr 2021 23:35:20 +0200 clarified conditional ML;
wenzelm [Fri, 16 Apr 2021 23:35:20 +0200] rev 73587
clarified conditional ML;
Fri, 16 Apr 2021 23:16:00 +0200 support for conditional ML text;
wenzelm [Fri, 16 Apr 2021 23:16:00 +0200] rev 73586
support for conditional ML text;
Fri, 16 Apr 2021 21:54:08 +0200 updated example;
wenzelm [Fri, 16 Apr 2021 21:54:08 +0200] rev 73585
updated example;
Fri, 16 Apr 2021 21:50:47 +0200 clarified options;
wenzelm [Fri, 16 Apr 2021 21:50:47 +0200] rev 73584
clarified options;
Thu, 15 Apr 2021 19:45:43 +0000 proper context variable handling when stripping leadings quantifiers from test goals
haftmann [Thu, 15 Apr 2021 19:45:43 +0000] rev 73583
proper context variable handling when stripping leadings quantifiers from test goals
Wed, 14 Apr 2021 21:15:24 +0200 proper etc/ISABELLE_ID from archive (amending 4cba4e250c28);
wenzelm [Wed, 14 Apr 2021 21:15:24 +0200] rev 73582
proper etc/ISABELLE_ID from archive (amending 4cba4e250c28);
Wed, 14 Apr 2021 20:53:28 +0200 eliminated perl: prefer elementary GNU printenv;
wenzelm [Wed, 14 Apr 2021 20:53:28 +0200] rev 73581
eliminated perl: prefer elementary GNU printenv;
Wed, 14 Apr 2021 14:36:13 +0200 more robust bootstrap of components;
wenzelm [Wed, 14 Apr 2021 14:36:13 +0200] rev 73580
more robust bootstrap of components;
Wed, 14 Apr 2021 14:28:30 +0200 more self-contained support for macOS;
wenzelm [Wed, 14 Apr 2021 14:28:30 +0200] rev 73579
more self-contained support for macOS;
Tue, 13 Apr 2021 16:19:43 +0200 misc tuning and clarification;
wenzelm [Tue, 13 Apr 2021 16:19:43 +0200] rev 73578
misc tuning and clarification;
Tue, 13 Apr 2021 11:44:47 +0200 tuned signature;
wenzelm [Tue, 13 Apr 2021 11:44:47 +0200] rev 73577
tuned signature;
Mon, 12 Apr 2021 22:57:39 +0200 support for base64 via Isabelle/Scala/ML;
wenzelm [Mon, 12 Apr 2021 22:57:39 +0200] rev 73576
support for base64 via Isabelle/Scala/ML;
Mon, 12 Apr 2021 22:45:38 +0200 compile;
wenzelm [Mon, 12 Apr 2021 22:45:38 +0200] rev 73575
compile;
Mon, 12 Apr 2021 22:41:51 +0200 clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm [Mon, 12 Apr 2021 22:41:51 +0200] rev 73574
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
Mon, 12 Apr 2021 22:36:13 +0200 clarified signature (again);
wenzelm [Mon, 12 Apr 2021 22:36:13 +0200] rev 73573
clarified signature (again);
Mon, 12 Apr 2021 22:26:30 +0200 merged
wenzelm [Mon, 12 Apr 2021 22:26:30 +0200] rev 73572
merged
Mon, 12 Apr 2021 22:26:09 +0200 clarified signature;
wenzelm [Mon, 12 Apr 2021 22:26:09 +0200] rev 73571
clarified signature;
Mon, 12 Apr 2021 22:18:37 +0200 unused;
wenzelm [Mon, 12 Apr 2021 22:18:37 +0200] rev 73570
unused;
Mon, 12 Apr 2021 22:17:48 +0200 unused;
wenzelm [Mon, 12 Apr 2021 22:17:48 +0200] rev 73569
unused;
Mon, 12 Apr 2021 22:16:31 +0200 clarified signature: more structured arguments, notably for remote provers;
wenzelm [Mon, 12 Apr 2021 22:16:31 +0200] rev 73568
clarified signature: more structured arguments, notably for remote provers;
Mon, 12 Apr 2021 21:48:04 +0200 clarified signature;
wenzelm [Mon, 12 Apr 2021 21:48:04 +0200] rev 73567
clarified signature;
Mon, 12 Apr 2021 18:29:34 +0200 clarified signature: avoid tmp file;
wenzelm [Mon, 12 Apr 2021 18:29:34 +0200] rev 73566
clarified signature: avoid tmp file;
Mon, 12 Apr 2021 18:10:13 +0200 clarified signature for Scala functions;
wenzelm [Mon, 12 Apr 2021 18:10:13 +0200] rev 73565
clarified signature for Scala functions;
Mon, 12 Apr 2021 15:00:03 +0200 clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
wenzelm [Mon, 12 Apr 2021 15:00:03 +0200] rev 73564
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
Mon, 12 Apr 2021 14:14:47 +0200 tuned;
wenzelm [Mon, 12 Apr 2021 14:14:47 +0200] rev 73563
tuned;
Mon, 12 Apr 2021 12:32:09 +0200 clarified cache;
wenzelm [Mon, 12 Apr 2021 12:32:09 +0200] rev 73562
clarified cache;
Mon, 12 Apr 2021 12:16:49 +0200 clarified signature: Bytes extends CharSequence already (see d201996f72a8);
wenzelm [Mon, 12 Apr 2021 12:16:49 +0200] rev 73561
clarified signature: Bytes extends CharSequence already (see d201996f72a8);
Mon, 12 Apr 2021 11:45:16 +0200 clarified exceptions;
wenzelm [Mon, 12 Apr 2021 11:45:16 +0200] rev 73560
clarified exceptions;
Sun, 11 Apr 2021 22:47:55 +0200 more uniform use of Byte_Message;
wenzelm [Sun, 11 Apr 2021 22:47:55 +0200] rev 73559
more uniform use of Byte_Message; support protocol_message with multiple chunks;
Sun, 11 Apr 2021 21:32:09 +0200 tuned signature;
wenzelm [Sun, 11 Apr 2021 21:32:09 +0200] rev 73558
tuned signature;
Sun, 11 Apr 2021 21:23:51 +0200 tuned signature;
wenzelm [Sun, 11 Apr 2021 21:23:51 +0200] rev 73557
tuned signature;
Sat, 10 Apr 2021 21:50:59 +0200 more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm [Sat, 10 Apr 2021 21:50:59 +0200] rev 73556
more robust treatment of empty markup: it allows to produce formal chunks;
Sun, 11 Apr 2021 07:35:24 +0000 collected combinatorial material
haftmann [Sun, 11 Apr 2021 07:35:24 +0000] rev 73555
collected combinatorial material
Sat, 10 Apr 2021 20:22:07 +0200 tuned;
wenzelm [Sat, 10 Apr 2021 20:22:07 +0200] rev 73554
tuned;
Sat, 10 Apr 2021 19:45:51 +0200 tuned;
wenzelm [Sat, 10 Apr 2021 19:45:51 +0200] rev 73553
tuned;
Sat, 10 Apr 2021 14:56:03 +0200 more documentation;
wenzelm [Sat, 10 Apr 2021 14:56:03 +0200] rev 73552
more documentation;
Sat, 10 Apr 2021 14:55:50 +0200 proper treatment of nested antiquotations;
wenzelm [Sat, 10 Apr 2021 14:55:50 +0200] rev 73551
proper treatment of nested antiquotations; clarified signature;
Fri, 09 Apr 2021 22:06:59 +0200 support for ML special forms: modified evaluation similar to Scheme;
wenzelm [Fri, 09 Apr 2021 22:06:59 +0200] rev 73550
support for ML special forms: modified evaluation similar to Scheme;
Fri, 09 Apr 2021 21:07:11 +0200 clarified signature: more detailed token positions for antiquotations;
wenzelm [Fri, 09 Apr 2021 21:07:11 +0200] rev 73549
clarified signature: more detailed token positions for antiquotations;
Thu, 08 Apr 2021 20:52:19 +0200 merged
wenzelm [Thu, 08 Apr 2021 20:52:19 +0200] rev 73548
merged
Thu, 08 Apr 2021 16:43:35 +0200 clarified signature;
wenzelm [Thu, 08 Apr 2021 16:43:35 +0200] rev 73547
clarified signature;
Thu, 08 Apr 2021 12:38:18 +0000 confluent preprocessing for floats in presence of target language numerals
haftmann [Thu, 08 Apr 2021 12:38:18 +0000] rev 73546
confluent preprocessing for floats in presence of target language numerals
Wed, 07 Apr 2021 15:46:06 +0000 subclass relation
haftmann [Wed, 07 Apr 2021 15:46:06 +0000] rev 73545
subclass relation
Wed, 07 Apr 2021 22:32:43 +0200 some tinkering with npm versions;
wenzelm [Wed, 07 Apr 2021 22:32:43 +0200] rev 73544
some tinkering with npm versions;
Wed, 07 Apr 2021 22:28:41 +0200 some tinkering with npm versions;
wenzelm [Wed, 07 Apr 2021 22:28:41 +0200] rev 73543
some tinkering with npm versions;
Wed, 07 Apr 2021 18:13:02 +0200 back to post-release mode;
wenzelm [Wed, 07 Apr 2021 18:13:02 +0200] rev 73542
back to post-release mode;
Wed, 07 Apr 2021 18:05:48 +0200 tuned signature;
wenzelm [Wed, 07 Apr 2021 18:05:48 +0200] rev 73541
tuned signature;
Wed, 07 Apr 2021 18:05:14 +0200 auto-update due to "isabelle build_vscode";
wenzelm [Wed, 07 Apr 2021 18:05:14 +0200] rev 73540
auto-update due to "isabelle build_vscode";
Wed, 07 Apr 2021 18:04:45 +0200 tuned;
wenzelm [Wed, 07 Apr 2021 18:04:45 +0200] rev 73539
tuned;
Wed, 07 Apr 2021 18:04:30 +0200 tuned --- following hints by IntelliJ IDEA;
wenzelm [Wed, 07 Apr 2021 18:04:30 +0200] rev 73538
tuned --- following hints by IntelliJ IDEA;
Wed, 07 Apr 2021 11:05:00 +0200 fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes)
Manuel Eberl <eberlm@in.tum.de> [Wed, 07 Apr 2021 11:05:00 +0200] rev 73537
fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes)
Wed, 07 Apr 2021 12:28:19 +0000 simplified definition
haftmann [Wed, 07 Apr 2021 12:28:19 +0000] rev 73536
simplified definition
Tue, 06 Apr 2021 18:12:20 +0000 new lemmas
haftmann [Tue, 06 Apr 2021 18:12:20 +0000] rev 73535
new lemmas
Mon, 05 Apr 2021 22:46:41 +0200 discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove";
wenzelm [Mon, 05 Apr 2021 22:46:41 +0200] rev 73534
discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove";
Mon, 05 Apr 2021 22:45:01 +0200 following recent Phabricator update, after 2021 Week 13 (Late March);
wenzelm [Mon, 05 Apr 2021 22:45:01 +0200] rev 73533
following recent Phabricator update, after 2021 Week 13 (Late March);
Fri, 02 Apr 2021 12:24:35 +0100 merged
paulson [Fri, 02 Apr 2021 12:24:35 +0100] rev 73532
merged
Fri, 02 Apr 2021 12:24:29 +0100 Cosmetic: no !! in the lemma statement
paulson <lp15@cam.ac.uk> [Fri, 02 Apr 2021 12:24:29 +0100] rev 73531
Cosmetic: no !! in the lemma statement
Thu, 01 Apr 2021 19:14:43 +0200 clarified README;
wenzelm [Thu, 01 Apr 2021 19:14:43 +0200] rev 73530
clarified README; avoid odd patching of sources;
Thu, 01 Apr 2021 19:07:06 +0200 more standard header, with utf-8 encoding;
wenzelm [Thu, 01 Apr 2021 19:07:06 +0200] rev 73529
more standard header, with utf-8 encoding;
Thu, 01 Apr 2021 19:01:19 +0200 clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;
wenzelm [Thu, 01 Apr 2021 19:01:19 +0200] rev 73528
clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;
Thu, 01 Apr 2021 07:35:03 +0200 merged
nipkow [Thu, 01 Apr 2021 07:35:03 +0200] rev 73527
merged
Wed, 31 Mar 2021 18:18:03 +0200 new automatic order prover: stateless, complete, verified
nipkow [Wed, 31 Mar 2021 18:18:03 +0200] rev 73526
new automatic order prover: stateless, complete, verified
Wed, 31 Mar 2021 23:45:16 +0200 clarified signature;
wenzelm [Wed, 31 Mar 2021 23:45:16 +0200] rev 73525
clarified signature;
Wed, 31 Mar 2021 23:13:13 +0200 clarified: follow "isabelle version -t";
wenzelm [Wed, 31 Mar 2021 23:13:13 +0200] rev 73524
clarified: follow "isabelle version -t";
Wed, 31 Mar 2021 22:58:17 +0200 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm [Wed, 31 Mar 2021 22:58:17 +0200] rev 73523
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
Wed, 31 Mar 2021 22:10:56 +0200 tuned signature -- more explicit types;
wenzelm [Wed, 31 Mar 2021 22:10:56 +0200] rev 73522
tuned signature -- more explicit types;
Wed, 31 Mar 2021 21:44:29 +0200 more robust and uniform ISABELLE_TAGS;
wenzelm [Wed, 31 Mar 2021 21:44:29 +0200] rev 73521
more robust and uniform ISABELLE_TAGS;
Wed, 31 Mar 2021 18:12:46 +0200 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm [Wed, 31 Mar 2021 18:12:46 +0200] rev 73520
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
Wed, 31 Mar 2021 17:15:54 +0200 simplified release status (again), in contrast to a43898f76ae9;
wenzelm [Wed, 31 Mar 2021 17:15:54 +0200] rev 73519
simplified release status (again), in contrast to a43898f76ae9;
Wed, 31 Mar 2021 12:02:52 +0200 more uniform HTTP resources;
wenzelm [Wed, 31 Mar 2021 12:02:52 +0200] rev 73518
more uniform HTTP resources;
Wed, 31 Mar 2021 11:24:46 +0200 clarified (again): local tip could be actually more recent;
wenzelm [Wed, 31 Mar 2021 11:24:46 +0200] rev 73517
clarified (again): local tip could be actually more recent;
Wed, 31 Mar 2021 11:21:08 +0200 tuned;
wenzelm [Wed, 31 Mar 2021 11:21:08 +0200] rev 73516
tuned;
Wed, 31 Mar 2021 11:17:45 +0200 tuned;
wenzelm [Wed, 31 Mar 2021 11:17:45 +0200] rev 73515
tuned;
Wed, 31 Mar 2021 11:05:40 +0200 clarified name;
wenzelm [Wed, 31 Mar 2021 11:05:40 +0200] rev 73514
clarified name;
Wed, 31 Mar 2021 10:57:18 +0200 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm [Wed, 31 Mar 2021 10:57:18 +0200] rev 73513
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
Tue, 30 Mar 2021 12:32:24 +0200 support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm [Tue, 30 Mar 2021 12:32:24 +0200] rev 73512
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
Tue, 30 Mar 2021 09:42:25 +0200 updated to latest latex due to new mechanism for dealing with bold ccfonts
nipkow [Tue, 30 Mar 2021 09:42:25 +0200] rev 73511
updated to latest latex due to new mechanism for dealing with bold ccfonts
Mon, 29 Mar 2021 12:26:13 +0100 removal of needless hypothesis in hd_rev and last_rev
paulson <lp15@cam.ac.uk> [Mon, 29 Mar 2021 12:26:13 +0100] rev 73510
removal of needless hypothesis in hd_rev and last_rev
Sun, 28 Mar 2021 12:21:37 +0200 more robust;
wenzelm [Sun, 28 Mar 2021 12:21:37 +0200] rev 73509
more robust;
Sun, 28 Mar 2021 12:10:14 +0200 clarified message;
wenzelm [Sun, 28 Mar 2021 12:10:14 +0200] rev 73508
clarified message;
Sun, 28 Mar 2021 12:08:43 +0200 tuned;
wenzelm [Sun, 28 Mar 2021 12:08:43 +0200] rev 73507
tuned;
Sun, 28 Mar 2021 12:07:46 +0200 tuned message;
wenzelm [Sun, 28 Mar 2021 12:07:46 +0200] rev 73506
tuned message;
Sun, 28 Mar 2021 12:02:20 +0200 proper export;
wenzelm [Sun, 28 Mar 2021 12:02:20 +0200] rev 73505
proper export;
Sun, 28 Mar 2021 11:59:30 +0200 more options: build is part of default setup;
wenzelm [Sun, 28 Mar 2021 11:59:30 +0200] rev 73504
more options: build is part of default setup;
Sun, 28 Mar 2021 11:45:00 +0200 misc tuning and clarification;
wenzelm [Sun, 28 Mar 2021 11:45:00 +0200] rev 73503
misc tuning and clarification;
Sun, 28 Mar 2021 11:39:53 +0200 more options;
wenzelm [Sun, 28 Mar 2021 11:39:53 +0200] rev 73502
more options;
Sun, 28 Mar 2021 11:35:08 +0200 proper Admin script, outside the settings environment;
wenzelm [Sun, 28 Mar 2021 11:35:08 +0200] rev 73501
proper Admin script, outside the settings environment;
Sun, 28 Mar 2021 11:33:30 +0200 tuned whitespace;
wenzelm [Sun, 28 Mar 2021 11:33:30 +0200] rev 73500
tuned whitespace;
Sat, 27 Mar 2021 23:03:57 +0100 tuned;
wenzelm [Sat, 27 Mar 2021 23:03:57 +0100] rev 73499
tuned;
Sat, 27 Mar 2021 22:59:12 +0100 clarified;
wenzelm [Sat, 27 Mar 2021 22:59:12 +0100] rev 73498
clarified;
Sat, 27 Mar 2021 22:48:59 +0100 tuned message;
wenzelm [Sat, 27 Mar 2021 22:48:59 +0100] rev 73497
tuned message;
Sat, 27 Mar 2021 22:48:15 +0100 tuned message;
wenzelm [Sat, 27 Mar 2021 22:48:15 +0100] rev 73496
tuned message;
Sat, 27 Mar 2021 22:36:45 +0100 more accurate settings after update of current version;
wenzelm [Sat, 27 Mar 2021 22:36:45 +0100] rev 73495
more accurate settings after update of current version;
Sat, 27 Mar 2021 22:26:13 +0100 clarified messages;
wenzelm [Sat, 27 Mar 2021 22:26:13 +0100] rev 73494
clarified messages;
Sat, 27 Mar 2021 22:19:56 +0100 more robust: lest hg work out remote tip;
wenzelm [Sat, 27 Mar 2021 22:19:56 +0100] rev 73493
more robust: lest hg work out remote tip; more options;
Sat, 27 Mar 2021 22:09:49 +0100 more options;
wenzelm [Sat, 27 Mar 2021 22:09:49 +0100] rev 73492
more options;
Sat, 27 Mar 2021 21:27:27 +0100 clarified treatment of multiple versions: last one counts;
wenzelm [Sat, 27 Mar 2021 21:27:27 +0100] rev 73491
clarified treatment of multiple versions: last one counts; more options;
Sat, 27 Mar 2021 20:53:11 +0100 more robust;
wenzelm [Sat, 27 Mar 2021 20:53:11 +0100] rev 73490
more robust;
Sat, 27 Mar 2021 20:39:14 +0100 more robust: explicit repository root;
wenzelm [Sat, 27 Mar 2021 20:39:14 +0100] rev 73489
more robust: explicit repository root;
Sat, 27 Mar 2021 20:37:49 +0100 more robust;
wenzelm [Sat, 27 Mar 2021 20:37:49 +0100] rev 73488
more robust;
Sat, 27 Mar 2021 20:24:04 +0100 more convenient repository setup;
wenzelm [Sat, 27 Mar 2021 20:24:04 +0100] rev 73487
more convenient repository setup;
Sat, 27 Mar 2021 19:46:02 +0100 tuned;
wenzelm [Sat, 27 Mar 2021 19:46:02 +0100] rev 73486
tuned;
Sat, 27 Mar 2021 19:44:36 +0100 more robust invocation of hg;
wenzelm [Sat, 27 Mar 2021 19:44:36 +0100] rev 73485
more robust invocation of hg;
Sat, 27 Mar 2021 19:26:34 +0100 more robust: idempotent;
wenzelm [Sat, 27 Mar 2021 19:26:34 +0100] rev 73484
more robust: idempotent;
Sat, 27 Mar 2021 18:15:19 +0100 more robust invocation of hg;
wenzelm [Sat, 27 Mar 2021 18:15:19 +0100] rev 73483
more robust invocation of hg;
Sat, 27 Mar 2021 18:03:50 +0100 tuned;
wenzelm [Sat, 27 Mar 2021 18:03:50 +0100] rev 73482
tuned;
Sat, 27 Mar 2021 18:01:41 +0100 clarified output;
wenzelm [Sat, 27 Mar 2021 18:01:41 +0100] rev 73481
clarified output; more options;
Sat, 27 Mar 2021 17:13:15 +0100 support repository archives (without full .hg directory);
wenzelm [Sat, 27 Mar 2021 17:13:15 +0100] rev 73480
support repository archives (without full .hg directory);
Sat, 27 Mar 2021 17:05:36 +0100 more robust invocation of hg;
wenzelm [Sat, 27 Mar 2021 17:05:36 +0100] rev 73479
more robust invocation of hg;
Sat, 27 Mar 2021 15:56:49 +0100 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);
wenzelm [Sat, 27 Mar 2021 15:56:49 +0100] rev 73478
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);
Thu, 25 Mar 2021 08:52:15 +0000 dedicated session for combinatorial material
haftmann [Thu, 25 Mar 2021 08:52:15 +0000] rev 73477
dedicated session for combinatorial material
Wed, 24 Mar 2021 21:17:19 +0100 support for Java Chromium Embedded Framework (JCEF): still somewhat fragile;
wenzelm [Wed, 24 Mar 2021 21:17:19 +0100] rev 73476
support for Java Chromium Embedded Framework (JCEF): still somewhat fragile;
Tue, 23 Mar 2021 19:47:15 +0100 enforce full build;
wenzelm [Tue, 23 Mar 2021 19:47:15 +0100] rev 73475
enforce full build;
Tue, 23 Mar 2021 13:27:15 +0100 turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont;
wenzelm [Tue, 23 Mar 2021 13:27:15 +0100] rev 73474
turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont;
Tue, 23 Mar 2021 13:13:31 +0100 discontinue fragile check in LaTeX, e.g. problems with toc entries;
wenzelm [Tue, 23 Mar 2021 13:13:31 +0100] rev 73473
discontinue fragile check in LaTeX, e.g. problems with toc entries;
Mon, 22 Mar 2021 21:24:25 +0000 merged
paulson [Mon, 22 Mar 2021 21:24:25 +0000] rev 73472
merged
Mon, 22 Mar 2021 12:18:43 +0000 merged
paulson [Mon, 22 Mar 2021 12:18:43 +0000] rev 73471
merged
Mon, 22 Mar 2021 12:18:35 +0000 type class relaxation
paulson <lp15@cam.ac.uk> [Mon, 22 Mar 2021 12:18:35 +0000] rev 73470
type class relaxation
Mon, 22 Mar 2021 17:33:08 +0100 more NEWS;
wenzelm [Mon, 22 Mar 2021 17:33:08 +0100] rev 73469
more NEWS;
Mon, 22 Mar 2021 17:28:07 +0100 clarified group (but hard to tell);
wenzelm [Mon, 22 Mar 2021 17:28:07 +0100] rev 73468
clarified group (but hard to tell);
Mon, 22 Mar 2021 17:24:42 +0100 more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
wenzelm [Mon, 22 Mar 2021 17:24:42 +0100] rev 73467
more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd; corresponding symbols and latex macros;
Mon, 22 Mar 2021 10:49:51 +0000 more lemmas
haftmann [Mon, 22 Mar 2021 10:49:51 +0000] rev 73466
more lemmas
Mon, 22 Mar 2021 00:07:55 +0100 clarified package name (actually both pxfonts and txfonts exist and have this font);
wenzelm [Mon, 22 Mar 2021 00:07:55 +0100] rev 73465
clarified package name (actually both pxfonts and txfonts exist and have this font);
Sun, 21 Mar 2021 23:56:54 +0100 tuned;
wenzelm [Sun, 21 Mar 2021 23:56:54 +0100] rev 73464
tuned;
Sun, 21 Mar 2021 23:24:20 +0100 prefer isabelle bbbfont;
wenzelm [Sun, 21 Mar 2021 23:24:20 +0100] rev 73463
prefer isabelle bbbfont;
Sun, 21 Mar 2021 23:16:34 +0100 enforce full build;
wenzelm [Sun, 21 Mar 2021 23:16:34 +0100] rev 73462
enforce full build;
Sun, 21 Mar 2021 23:15:55 +0100 clarified symbol names, notably relevant for Z_Notation;
wenzelm [Sun, 21 Mar 2021 23:15:55 +0100] rev 73461
clarified symbol names, notably relevant for Z_Notation;
Sun, 21 Mar 2021 23:05:17 +0100 update README (actually after update of component);
wenzelm [Sun, 21 Mar 2021 23:05:17 +0100] rev 73460
update README (actually after update of component);
Sun, 21 Mar 2021 23:03:31 +0100 high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm [Sun, 21 Mar 2021 23:03:31 +0100] rev 73459
high-quality blackboard-bold fonts from "txmia" (package "txfonts");
Fri, 19 Mar 2021 23:37:12 +0100 publish component;
wenzelm [Fri, 19 Mar 2021 23:37:12 +0100] rev 73458
publish component;
Fri, 19 Mar 2021 23:35:37 +0100 further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
wenzelm [Fri, 19 Mar 2021 23:35:37 +0100] rev 73457
further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
Fri, 19 Mar 2021 13:44:33 +0100 clarified \<Zcomp> (small) vs. \<Zsemi> (big);
wenzelm [Fri, 19 Mar 2021 13:44:33 +0100] rev 73456
clarified \<Zcomp> (small) vs. \<Zsemi> (big);
Fri, 19 Mar 2021 13:22:12 +0100 more CONTRIBUTORS;
wenzelm [Fri, 19 Mar 2021 13:22:12 +0100] rev 73455
more CONTRIBUTORS;
Fri, 19 Mar 2021 12:35:55 +0100 more Z_Notation symbols, as proposed by Simon Foster;
wenzelm [Fri, 19 Mar 2021 12:35:55 +0100] rev 73454
more Z_Notation symbols, as proposed by Simon Foster; some LaTeX-art based on tex.stackexchange "How do you make a square element symbol (\in)";
Thu, 18 Mar 2021 21:49:19 +0100 more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus";
wenzelm [Thu, 18 Mar 2021 21:49:19 +0100] rev 73453
more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus";
Thu, 18 Mar 2021 21:36:19 +0100 clarified order for GUI panel;
wenzelm [Thu, 18 Mar 2021 21:36:19 +0100] rev 73452
clarified order for GUI panel;
Thu, 18 Mar 2021 06:37:24 +0000 prefer more direct interpretation
haftmann [Thu, 18 Mar 2021 06:37:24 +0000] rev 73451
prefer more direct interpretation
Thu, 18 Mar 2021 13:03:29 +0100 more Z_Notation symbols, as proposed by Simon Foster;
wenzelm [Thu, 18 Mar 2021 13:03:29 +0100] rev 73450
more Z_Notation symbols, as proposed by Simon Foster;
Thu, 18 Mar 2021 12:53:05 +0100 more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt;
wenzelm [Thu, 18 Mar 2021 12:53:05 +0100] rev 73449
more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt;
Thu, 18 Mar 2021 12:46:25 +0100 clarified order for presentation in isar-ref (Appendix B);
wenzelm [Thu, 18 Mar 2021 12:46:25 +0100] rev 73448
clarified order for presentation in isar-ref (Appendix B);
Thu, 18 Mar 2021 12:41:17 +0100 prefer explicit \<Zproject> (with its own Unicode codepoint);
wenzelm [Thu, 18 Mar 2021 12:41:17 +0100] rev 73447
prefer explicit \<Zproject> (with its own Unicode codepoint);
Wed, 17 Mar 2021 22:24:57 +0100 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm [Wed, 17 Mar 2021 22:24:57 +0100] rev 73446
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster; NB: no bold version of 0x2900 due to fontforge crash "Internal Error: Some fragments did not join";
Tue, 16 Mar 2021 23:30:51 +0100 tuned message;
wenzelm [Tue, 16 Mar 2021 23:30:51 +0100] rev 73445
tuned message;
Tue, 16 Mar 2021 22:13:04 +0100 proper directory of settings file;
wenzelm [Tue, 16 Mar 2021 22:13:04 +0100] rev 73444
proper directory of settings file; tuned;
Tue, 16 Mar 2021 08:42:21 +0100 tuned lemma
nipkow [Tue, 16 Mar 2021 08:42:21 +0100] rev 73443
tuned lemma
Mon, 15 Mar 2021 22:58:20 +0100 added lemma
nipkow [Mon, 15 Mar 2021 22:58:20 +0100] rev 73442
added lemma
Mon, 15 Mar 2021 11:50:58 +0100 tuned signature;
wenzelm [Mon, 15 Mar 2021 11:50:58 +0100] rev 73441
tuned signature;
Mon, 15 Mar 2021 11:43:56 +0100 tuned signature (again);
wenzelm [Mon, 15 Mar 2021 11:43:56 +0100] rev 73440
tuned signature (again);
Sun, 14 Mar 2021 22:55:52 +0100 tuned --- following hints by IntelliJ;
wenzelm [Sun, 14 Mar 2021 22:55:52 +0100] rev 73439
tuned --- following hints by IntelliJ;
Sun, 14 Mar 2021 22:34:41 +0100 tuned comments;
wenzelm [Sun, 14 Mar 2021 22:34:41 +0100] rev 73438
tuned comments;
Sun, 14 Mar 2021 21:41:28 +0100 proper shell quote;
wenzelm [Sun, 14 Mar 2021 21:41:28 +0100] rev 73437
proper shell quote;
Sun, 14 Mar 2021 21:02:34 +0100 removed spurious references to perl / libwww-perl;
wenzelm [Sun, 14 Mar 2021 21:02:34 +0100] rev 73436
removed spurious references to perl / libwww-perl;
Sun, 14 Mar 2021 20:29:26 +0100 invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm [Sun, 14 Mar 2021 20:29:26 +0100] rev 73435
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl); clarified inlined command-line; clarified errors: exception ERROR becomes UnknownError (it could stem from Scala function);
Sun, 14 Mar 2021 18:32:11 +0100 clarified signature: refer to file name instead of file content;
wenzelm [Sun, 14 Mar 2021 18:32:11 +0100] rev 73434
clarified signature: refer to file name instead of file content;
Sun, 14 Mar 2021 18:27:55 +0100 compile;
wenzelm [Sun, 14 Mar 2021 18:27:55 +0100] rev 73433
compile;
Sun, 14 Mar 2021 16:50:11 +0100 clarified signature: more explicit types;
wenzelm [Sun, 14 Mar 2021 16:50:11 +0100] rev 73432
clarified signature: more explicit types;
Sun, 14 Mar 2021 15:28:44 +0100 support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm [Sun, 14 Mar 2021 15:28:44 +0100] rev 73431
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
Sun, 14 Mar 2021 13:21:59 +0100 clarified signature;
wenzelm [Sun, 14 Mar 2021 13:21:59 +0100] rev 73430
clarified signature;
Sun, 14 Mar 2021 13:09:17 +0100 elapsed time to download content (and for the server to provide content);
wenzelm [Sun, 14 Mar 2021 13:09:17 +0100] rev 73429
elapsed time to download content (and for the server to provide content);
Sat, 13 Mar 2021 19:29:45 +0100 more direct elapsed run_time via bash_process wrapper (via Scala and C);
wenzelm [Sat, 13 Mar 2021 19:29:45 +0100] rev 73428
more direct elapsed run_time via bash_process wrapper (via Scala and C);
Sat, 13 Mar 2021 15:39:48 +0100 merged
wenzelm [Sat, 13 Mar 2021 15:39:48 +0100] rev 73427
merged
Sat, 13 Mar 2021 15:14:46 +0100 use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm [Sat, 13 Mar 2021 15:14:46 +0100] rev 73426
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
Sat, 13 Mar 2021 14:55:27 +0100 clarified signature: let Sledgehammer handle SystemOnTPTP comments;
wenzelm [Sat, 13 Mar 2021 14:55:27 +0100] rev 73425
clarified signature: let Sledgehammer handle SystemOnTPTP comments;
Sat, 13 Mar 2021 14:27:34 +0100 clarified signature: url may change dynamically and is part of result;
wenzelm [Sat, 13 Mar 2021 14:27:34 +0100] rev 73424
clarified signature: url may change dynamically and is part of result;
Sat, 13 Mar 2021 14:27:07 +0100 clarified error;
wenzelm [Sat, 13 Mar 2021 14:27:07 +0100] rev 73423
clarified error;
Sat, 13 Mar 2021 14:08:25 +0100 support timeout, similar to perl LWP::UserAgent;
wenzelm [Sat, 13 Mar 2021 14:08:25 +0100] rev 73422
support timeout, similar to perl LWP::UserAgent;
Sat, 13 Mar 2021 13:44:42 +0100 clarified signature;
wenzelm [Sat, 13 Mar 2021 13:44:42 +0100] rev 73421
clarified signature;
Sat, 13 Mar 2021 12:45:31 +0100 tuned;
wenzelm [Sat, 13 Mar 2021 12:45:31 +0100] rev 73420
tuned;
Sat, 13 Mar 2021 12:36:24 +0100 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm [Sat, 13 Mar 2021 12:36:24 +0100] rev 73419
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
Fri, 12 Mar 2021 23:30:35 +0100 support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm [Fri, 12 Mar 2021 23:30:35 +0100] rev 73418
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
Fri, 12 Mar 2021 23:00:01 +0100 clarified HTTP.Content: support encoding;
wenzelm [Fri, 12 Mar 2021 23:00:01 +0100] rev 73417
clarified HTTP.Content: support encoding; more realistic HTTP.Client operations;
Fri, 12 Mar 2021 19:46:37 +0100 clarified signature: more explicit HTTP operations;
wenzelm [Fri, 12 Mar 2021 19:46:37 +0100] rev 73416
clarified signature: more explicit HTTP operations;
Fri, 12 Mar 2021 19:43:49 +0100 tuned;
wenzelm [Fri, 12 Mar 2021 19:43:49 +0100] rev 73415
tuned;
Fri, 12 Mar 2021 19:42:18 +0100 more robust;
wenzelm [Fri, 12 Mar 2021 19:42:18 +0100] rev 73414
more robust;
Thu, 11 Mar 2021 20:30:56 +0100 clarified signature;
wenzelm [Thu, 11 Mar 2021 20:30:56 +0100] rev 73413
clarified signature;
Thu, 11 Mar 2021 12:16:17 +0100 clarified components;
wenzelm [Thu, 11 Mar 2021 12:16:17 +0100] rev 73412
clarified components;
Thu, 11 Mar 2021 07:05:38 +0000 avoid name clash
haftmann [Thu, 11 Mar 2021 07:05:38 +0000] rev 73411
avoid name clash
Thu, 11 Mar 2021 07:05:29 +0000 lemma
haftmann [Thu, 11 Mar 2021 07:05:29 +0000] rev 73410
lemma
Thu, 11 Mar 2021 11:22:25 +0100 tuned;
wenzelm [Thu, 11 Mar 2021 11:22:25 +0100] rev 73409
tuned;
Thu, 11 Mar 2021 10:25:04 +0100 another example for lift_bnf for quotients
traytel [Thu, 11 Mar 2021 10:25:04 +0100] rev 73408
another example for lift_bnf for quotients
Wed, 10 Mar 2021 21:55:28 +0100 merged
wenzelm [Wed, 10 Mar 2021 21:55:28 +0100] rev 73407
merged
Wed, 10 Mar 2021 20:09:26 +0100 proper \usepackage[T1]{fontenc};
wenzelm [Wed, 10 Mar 2021 20:09:26 +0100] rev 73406
proper \usepackage[T1]{fontenc};
Wed, 10 Mar 2021 19:03:24 +0100 more robust init: avoid spilling opam artifacts;
wenzelm [Wed, 10 Mar 2021 19:03:24 +0100] rev 73405
more robust init: avoid spilling opam artifacts;
Tue, 09 Mar 2021 21:11:05 +0100 proper type-setting of cartouches (requires T1);
wenzelm [Tue, 09 Mar 2021 21:11:05 +0100] rev 73404
proper type-setting of cartouches (requires T1); \usepackage[T1]{fontenc} is default for mkroot; \usepackage[utf8]{inputenc} is obsolete in lualatex;
Tue, 09 Mar 2021 20:00:44 +0100 provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04;
wenzelm [Tue, 09 Mar 2021 20:00:44 +0100] rev 73403
provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04;
Tue, 09 Mar 2021 18:52:24 +0100 more robust;
wenzelm [Tue, 09 Mar 2021 18:52:24 +0100] rev 73402
more robust; eliminated perl;
Tue, 09 Mar 2021 18:44:43 +0100 removed unused latex packages;
wenzelm [Tue, 09 Mar 2021 18:44:43 +0100] rev 73401
removed unused latex packages;
Tue, 09 Mar 2021 17:31:51 +0100 obsolete (see 0c837beeb5e7);
wenzelm [Tue, 09 Mar 2021 17:31:51 +0100] rev 73400
obsolete (see 0c837beeb5e7);
Tue, 09 Mar 2021 17:15:21 +0100 proper Isabelle/Scala tool --- avoid perl;
wenzelm [Tue, 09 Mar 2021 17:15:21 +0100] rev 73399
proper Isabelle/Scala tool --- avoid perl;
Tue, 09 Mar 2021 14:20:27 +0100 generalized confluence-based subdistributivity theorem for quotients;
traytel [Tue, 09 Mar 2021 14:20:27 +0100] rev 73398
generalized confluence-based subdistributivity theorem for quotients; new example that triggered the generalization
Tue, 09 Mar 2021 11:50:21 +0100 Backed out changeset 3fdb94d87e0e
desharna [Tue, 09 Mar 2021 11:50:21 +0100] rev 73397
Backed out changeset 3fdb94d87e0e
Tue, 09 Mar 2021 11:50:11 +0100 Backed out changeset b867b436f372
desharna [Tue, 09 Mar 2021 11:50:11 +0100] rev 73396
Backed out changeset b867b436f372
Sun, 07 Mar 2021 08:26:02 +0100 reduced dependencies on List_Permutation
haftmann [Sun, 07 Mar 2021 08:26:02 +0100] rev 73395
reduced dependencies on List_Permutation
Sun, 07 Mar 2021 08:24:24 +0100 follow corresponding precedence on sets
haftmann [Sun, 07 Mar 2021 08:24:24 +0100] rev 73394
follow corresponding precedence on sets
Sat, 06 Mar 2021 18:42:10 +0000 consolidated names
haftmann [Sat, 06 Mar 2021 18:42:10 +0000] rev 73393
consolidated names
Sat, 06 Mar 2021 18:42:10 +0000 reduced dependencies on theory List_Permutation
haftmann [Sat, 06 Mar 2021 18:42:10 +0000] rev 73392
reduced dependencies on theory List_Permutation
Fri, 05 Mar 2021 22:23:57 +0100 obsolete (see f3378101f555);
wenzelm [Fri, 05 Mar 2021 22:23:57 +0100] rev 73391
obsolete (see f3378101f555);
Fri, 05 Mar 2021 21:26:38 +0100 merged
wenzelm [Fri, 05 Mar 2021 21:26:38 +0100] rev 73390
merged
Fri, 05 Mar 2021 20:52:08 +0100 more direct unlimited smt_timeout;
wenzelm [Fri, 05 Mar 2021 20:52:08 +0100] rev 73389
more direct unlimited smt_timeout; update of certificates: generated command-line options are part of input / digest;
Fri, 05 Mar 2021 20:38:55 +0100 clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm [Fri, 05 Mar 2021 20:38:55 +0100] rev 73388
clarified smt: support Timeout.ignored and Timeout.scale_time;
Fri, 05 Mar 2021 17:29:49 +0100 clarified timeouts in Isabelle/ML;
wenzelm [Fri, 05 Mar 2021 17:29:49 +0100] rev 73387
clarified timeouts in Isabelle/ML;
Fri, 05 Mar 2021 17:02:32 +0100 tuned --- more elementary Time operations;
wenzelm [Fri, 05 Mar 2021 17:02:32 +0100] rev 73386
tuned --- more elementary Time operations;
Fri, 05 Mar 2021 16:45:16 +0100 removed unused/pointless operation: Time.start is the load/init time of this Scala module;
wenzelm [Fri, 05 Mar 2021 16:45:16 +0100] rev 73385
removed unused/pointless operation: Time.start is the load/init time of this Scala module;
Fri, 05 Mar 2021 16:44:04 +0100 obsolete;
wenzelm [Fri, 05 Mar 2021 16:44:04 +0100] rev 73384
obsolete;
Fri, 05 Mar 2021 16:09:42 +0100 clarified signature --- augment existing structure Time;
wenzelm [Fri, 05 Mar 2021 16:09:42 +0100] rev 73383
clarified signature --- augment existing structure Time;
Fri, 05 Mar 2021 13:48:23 +0100 rebuild SMT certificates from scratch;
wenzelm [Fri, 05 Mar 2021 13:48:23 +0100] rev 73382
rebuild SMT certificates from scratch;
Fri, 05 Mar 2021 15:01:59 +0100 added lemmas (sublist|prefix|suffix)_list_all
desharna [Fri, 05 Mar 2021 15:01:59 +0100] rev 73381
added lemmas (sublist|prefix|suffix)_list_all
Fri, 05 Mar 2021 14:23:14 +0100 added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While
desharna [Fri, 05 Mar 2021 14:23:14 +0100] rev 73380
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While
Fri, 05 Mar 2021 12:05:54 +0100 added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI
desharna [Fri, 05 Mar 2021 12:05:54 +0100] rev 73379
added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI
Fri, 05 Mar 2021 10:30:54 +0100 typo
haftmann [Fri, 05 Mar 2021 10:30:54 +0100] rev 73378
typo
Fri, 05 Mar 2021 08:22:34 +0100 merged
desharna [Fri, 05 Mar 2021 08:22:34 +0100] rev 73377
merged
Thu, 04 Mar 2021 18:38:56 +0100 added upper bound on monomorphisation duplicate instances
desharna [Thu, 04 Mar 2021 18:38:56 +0100] rev 73376
added upper bound on monomorphisation duplicate instances
Thu, 04 Mar 2021 11:06:39 +0100 tuned best_slices in atp_config
desharna [Thu, 04 Mar 2021 11:06:39 +0100] rev 73375
tuned best_slices in atp_config
Thu, 04 Mar 2021 10:10:44 +0100 tuned exec field in atp_config
desharna [Thu, 04 Mar 2021 10:10:44 +0100] rev 73374
tuned exec field in atp_config
Thu, 04 Mar 2021 22:46:44 +0100 removed junk;
wenzelm [Thu, 04 Mar 2021 22:46:44 +0100] rev 73373
removed junk;
Thu, 04 Mar 2021 22:44:31 +0100 tuned proofs;
wenzelm [Thu, 04 Mar 2021 22:44:31 +0100] rev 73372
tuned proofs;
Thu, 04 Mar 2021 22:03:33 +0100 enforce full build, after significant changes in Isabelle/Scala;
wenzelm [Thu, 04 Mar 2021 22:03:33 +0100] rev 73371
enforce full build, after significant changes in Isabelle/Scala;
Thu, 04 Mar 2021 22:02:44 +0100 clarified compiler options: show relevant warnings;
wenzelm [Thu, 04 Mar 2021 22:02:44 +0100] rev 73370
clarified compiler options: show relevant warnings;
Thu, 04 Mar 2021 22:01:53 +0100 tuned --- avoid compiler warnings;
wenzelm [Thu, 04 Mar 2021 22:01:53 +0100] rev 73369
tuned --- avoid compiler warnings;
Thu, 04 Mar 2021 21:19:05 +0100 clarified signature --- fewer warnings;
wenzelm [Thu, 04 Mar 2021 21:19:05 +0100] rev 73368
clarified signature --- fewer warnings;
Thu, 04 Mar 2021 21:04:27 +0100 clarified signature --- fewer warnings;
wenzelm [Thu, 04 Mar 2021 21:04:27 +0100] rev 73367
clarified signature --- fewer warnings;
Thu, 04 Mar 2021 19:55:52 +0100 tuned --- fewer warnings;
wenzelm [Thu, 04 Mar 2021 19:55:52 +0100] rev 73366
tuned --- fewer warnings;
Thu, 04 Mar 2021 18:04:16 +0100 more robust ordering (see also 88c96e836ed6);
wenzelm [Thu, 04 Mar 2021 18:04:16 +0100] rev 73365
more robust ordering (see also 88c96e836ed6);
Thu, 04 Mar 2021 16:23:34 +0100 proper scala.collection.immutable;
wenzelm [Thu, 04 Mar 2021 16:23:34 +0100] rev 73364
proper scala.collection.immutable;
Thu, 04 Mar 2021 16:08:30 +0100 tuned --- fewer warnings;
wenzelm [Thu, 04 Mar 2021 16:08:30 +0100] rev 73363
tuned --- fewer warnings;
Thu, 04 Mar 2021 15:59:28 +0100 tuned --- fewer warnings;
wenzelm [Thu, 04 Mar 2021 15:59:28 +0100] rev 73362
tuned --- fewer warnings;
Thu, 04 Mar 2021 15:52:08 +0100 tuned;
wenzelm [Thu, 04 Mar 2021 15:52:08 +0100] rev 73361
tuned;
Thu, 04 Mar 2021 15:49:15 +0100 tuned --- fewer warnings;
wenzelm [Thu, 04 Mar 2021 15:49:15 +0100] rev 73360
tuned --- fewer warnings;
Thu, 04 Mar 2021 15:41:46 +0100 tuned --- fewer warnings;
wenzelm [Thu, 04 Mar 2021 15:41:46 +0100] rev 73359
tuned --- fewer warnings;
Wed, 03 Mar 2021 22:48:46 +0100 tuned --- fewer warnings;
wenzelm [Wed, 03 Mar 2021 22:48:46 +0100] rev 73358
tuned --- fewer warnings;
Wed, 03 Mar 2021 22:31:11 +0100 tuned --- fewer warnings;
wenzelm [Wed, 03 Mar 2021 22:31:11 +0100] rev 73357
tuned --- fewer warnings;
Wed, 03 Mar 2021 22:28:03 +0100 more robust error;
wenzelm [Wed, 03 Mar 2021 22:28:03 +0100] rev 73356
more robust error;
Wed, 03 Mar 2021 21:58:29 +0100 tuned --- fewer warnings;
wenzelm [Wed, 03 Mar 2021 21:58:29 +0100] rev 73355
tuned --- fewer warnings;
Wed, 03 Mar 2021 21:37:20 +0100 tuned --- fewer warnings;
wenzelm [Wed, 03 Mar 2021 21:37:20 +0100] rev 73354
tuned --- fewer warnings;
Wed, 03 Mar 2021 21:19:36 +0100 tuned --- fewer warnings;
wenzelm [Wed, 03 Mar 2021 21:19:36 +0100] rev 73353
tuned --- fewer warnings;
Wed, 03 Mar 2021 20:56:30 +0100 updated to scala-2.13.5 (with scala-swing_2.13-3.0.0);
wenzelm [Wed, 03 Mar 2021 20:56:30 +0100] rev 73352
updated to scala-2.13.5 (with scala-swing_2.13-3.0.0);
Wed, 03 Mar 2021 16:54:21 +0100 slightly more efficient Term.fastype_of (only little impact in regular applications);
wenzelm [Wed, 03 Mar 2021 16:54:21 +0100] rev 73351
slightly more efficient Term.fastype_of (only little impact in regular applications);
Tue, 02 Mar 2021 08:09:05 +0000 reduced dependencies on theory List_Permutation
haftmann [Tue, 02 Mar 2021 08:09:05 +0000] rev 73350
reduced dependencies on theory List_Permutation
Mon, 01 Mar 2021 23:26:27 +0000 Merge
paulson <lp15@cam.ac.uk> [Mon, 01 Mar 2021 23:26:27 +0000] rev 73349
Merge
Mon, 01 Mar 2021 17:59:17 +0000 reverted simprule status on a new lemma
paulson <lp15@cam.ac.uk> [Mon, 01 Mar 2021 17:59:17 +0000] rev 73348
reverted simprule status on a new lemma
Mon, 01 Mar 2021 14:47:08 +0000 merged
paulson [Mon, 01 Mar 2021 14:47:08 +0000] rev 73347
merged
Mon, 01 Mar 2021 14:46:51 +0000 tiny bit of lemma hacking
paulson <lp15@cam.ac.uk> [Mon, 01 Mar 2021 14:46:51 +0000] rev 73346
tiny bit of lemma hacking
Mon, 01 Mar 2021 23:26:55 +0100 tuned --- fewer warnings;
wenzelm [Mon, 01 Mar 2021 23:26:55 +0100] rev 73345
tuned --- fewer warnings;
Mon, 01 Mar 2021 23:17:47 +0100 tuned --- fewer warnings;
wenzelm [Mon, 01 Mar 2021 23:17:47 +0100] rev 73344
tuned --- fewer warnings;
Mon, 01 Mar 2021 22:50:00 +0100 tuned --- avoid deprecated conversions between certain number type;
wenzelm [Mon, 01 Mar 2021 22:50:00 +0100] rev 73343
tuned --- avoid deprecated conversions between certain number type;
Mon, 01 Mar 2021 22:37:33 +0100 tuned --- avoid deprecated Predef.any2stringadd;
wenzelm [Mon, 01 Mar 2021 22:37:33 +0100] rev 73342
tuned --- avoid deprecated Predef.any2stringadd;
Mon, 01 Mar 2021 22:26:33 +0100 tuned --- silence odd warning;
wenzelm [Mon, 01 Mar 2021 22:26:33 +0100] rev 73341
tuned --- silence odd warning;
Mon, 01 Mar 2021 22:22:12 +0100 tuned --- fewer warnings;
wenzelm [Mon, 01 Mar 2021 22:22:12 +0100] rev 73340
tuned --- fewer warnings;
Mon, 01 Mar 2021 20:12:09 +0100 tuned --- fewer warnings;
wenzelm [Mon, 01 Mar 2021 20:12:09 +0100] rev 73339
tuned --- fewer warnings;
Mon, 01 Mar 2021 20:04:33 +0100 tuned --- fewer warnings;
wenzelm [Mon, 01 Mar 2021 20:04:33 +0100] rev 73338
tuned --- fewer warnings;
Mon, 01 Mar 2021 19:41:52 +0100 tuned --- fewer warnings;
wenzelm [Mon, 01 Mar 2021 19:41:52 +0100] rev 73337
tuned --- fewer warnings;
Mon, 01 Mar 2021 18:31:11 +0100 clarified signature, according to Isabelle/Scala;
wenzelm [Mon, 01 Mar 2021 18:31:11 +0100] rev 73336
clarified signature, according to Isabelle/Scala;
Mon, 01 Mar 2021 18:24:50 +0100 download more directly, via means of JVM;
wenzelm [Mon, 01 Mar 2021 18:24:50 +0100] rev 73335
download more directly, via means of JVM;
Mon, 01 Mar 2021 18:24:27 +0100 download on separate thread;
wenzelm [Mon, 01 Mar 2021 18:24:27 +0100] rev 73334
download on separate thread;
Mon, 01 Mar 2021 18:11:06 +0100 clarified signature;
wenzelm [Mon, 01 Mar 2021 18:11:06 +0100] rev 73333
clarified signature;
Mon, 01 Mar 2021 17:44:44 +0100 tuned;
wenzelm [Mon, 01 Mar 2021 17:44:44 +0100] rev 73332
tuned;
Mon, 01 Mar 2021 15:09:57 +0100 proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
wenzelm [Mon, 01 Mar 2021 15:09:57 +0100] rev 73331
proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
Mon, 01 Mar 2021 14:58:00 +0100 tuned signature;
wenzelm [Mon, 01 Mar 2021 14:58:00 +0100] rev 73330
tuned signature;
Mon, 01 Mar 2021 08:16:22 +0100 NEWS
haftmann [Mon, 01 Mar 2021 08:16:22 +0100] rev 73329
NEWS
Sun, 28 Feb 2021 20:13:07 +0000 lemma diffusion
haftmann [Sun, 28 Feb 2021 20:13:07 +0000] rev 73328
lemma diffusion
Sun, 28 Feb 2021 20:13:07 +0000 more connections between mset _ = mset _ and permutations
haftmann [Sun, 28 Feb 2021 20:13:07 +0000] rev 73327
more connections between mset _ = mset _ and permutations
Sun, 28 Feb 2021 20:13:07 +0000 dissolve theory with duplicated name from afp
haftmann [Sun, 28 Feb 2021 20:13:07 +0000] rev 73326
dissolve theory with duplicated name from afp
Sun, 28 Feb 2021 21:31:35 +0100 more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
wenzelm [Sun, 28 Feb 2021 21:31:35 +0100] rev 73325
more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
Sat, 27 Feb 2021 22:17:56 +0100 more Isabelle/ML/Scala operations;
wenzelm [Sat, 27 Feb 2021 22:17:56 +0100] rev 73324
more Isabelle/ML/Scala operations;
Sat, 27 Feb 2021 21:36:58 +0100 more Isabelle/ML/Scala operations;
wenzelm [Sat, 27 Feb 2021 21:36:58 +0100] rev 73323
more Isabelle/ML/Scala operations;
Sat, 27 Feb 2021 21:01:07 +0100 more Isabelle/ML/Scala operations;
wenzelm [Sat, 27 Feb 2021 21:01:07 +0100] rev 73322
more Isabelle/ML/Scala operations; clarified errors;
Sat, 27 Feb 2021 20:49:38 +0100 proper src1, amending 20157c8ab3f3;
wenzelm [Sat, 27 Feb 2021 20:49:38 +0100] rev 73321
proper src1, amending 20157c8ab3f3;
Sat, 27 Feb 2021 19:51:56 +0100 tuned;
wenzelm [Sat, 27 Feb 2021 19:51:56 +0100] rev 73320
tuned;
Sat, 27 Feb 2021 19:45:33 +0100 proper File.eq, amending df49ca5da9d0;
wenzelm [Sat, 27 Feb 2021 19:45:33 +0100] rev 73319
proper File.eq, amending df49ca5da9d0;
Sat, 27 Feb 2021 19:42:44 +0100 tuned;
wenzelm [Sat, 27 Feb 2021 19:42:44 +0100] rev 73318
tuned;
Sat, 27 Feb 2021 18:04:29 +0100 clarified modules: more like ML;
wenzelm [Sat, 27 Feb 2021 18:04:29 +0100] rev 73317
clarified modules: more like ML;
Sat, 27 Feb 2021 17:33:40 +0100 obsolete;
wenzelm [Sat, 27 Feb 2021 17:33:40 +0100] rev 73316
obsolete;
Sat, 27 Feb 2021 17:32:02 +0100 tuned;
wenzelm [Sat, 27 Feb 2021 17:32:02 +0100] rev 73315
tuned;
Sat, 27 Feb 2021 17:25:54 +0100 more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm [Sat, 27 Feb 2021 17:25:54 +0100] rev 73314
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
Sat, 27 Feb 2021 16:33:16 +0100 discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working;
wenzelm [Sat, 27 Feb 2021 16:33:16 +0100] rev 73313
discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working;
Sat, 27 Feb 2021 13:39:06 +0100 more checks;
wenzelm [Sat, 27 Feb 2021 13:39:06 +0100] rev 73312
more checks;
Sat, 27 Feb 2021 13:37:04 +0100 clarified message;
wenzelm [Sat, 27 Feb 2021 13:37:04 +0100] rev 73311
clarified message;
Sat, 27 Feb 2021 13:20:52 +0100 clarified message;
wenzelm [Sat, 27 Feb 2021 13:20:52 +0100] rev 73310
clarified message;
Sat, 27 Feb 2021 13:01:36 +0100 clarified comments;
wenzelm [Sat, 27 Feb 2021 13:01:36 +0100] rev 73309
clarified comments;
Sat, 27 Feb 2021 11:51:39 +0100 clarified message;
wenzelm [Sat, 27 Feb 2021 11:51:39 +0100] rev 73308
clarified message;
Fri, 26 Feb 2021 11:46:58 +0100 improved list_neq simproc
nipkow [Fri, 26 Feb 2021 11:46:58 +0100] rev 73307
improved list_neq simproc
Thu, 25 Feb 2021 13:35:54 +0100 merged
haftmann [Thu, 25 Feb 2021 13:35:54 +0100] rev 73306
merged
Wed, 24 Feb 2021 21:45:09 +0100 repaired document
haftmann [Wed, 24 Feb 2021 21:45:09 +0100] rev 73305
repaired document
Wed, 24 Feb 2021 18:41:39 +0000 merged
paulson [Wed, 24 Feb 2021 18:41:39 +0000] rev 73304
merged
Wed, 24 Feb 2021 14:49:36 +0000 merged
paulson [Wed, 24 Feb 2021 14:49:36 +0000] rev 73303
merged
Wed, 24 Feb 2021 14:49:16 +0000 A couple of basic lemmas about arg
paulson <lp15@cam.ac.uk> [Wed, 24 Feb 2021 14:49:16 +0000] rev 73302
A couple of basic lemmas about arg
Wed, 24 Feb 2021 13:31:33 +0000 multiset as equivalence class of permuted lists
haftmann [Wed, 24 Feb 2021 13:31:33 +0000] rev 73301
multiset as equivalence class of permuted lists
Wed, 24 Feb 2021 13:31:28 +0000 emphasize connection to multisets
haftmann [Wed, 24 Feb 2021 13:31:28 +0000] rev 73300
emphasize connection to multisets
Wed, 24 Feb 2021 18:54:53 +0100 proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work;
wenzelm [Wed, 24 Feb 2021 18:54:53 +0100] rev 73299
proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work;
Tue, 23 Feb 2021 23:00:08 +0100 more on Isabelle_System.bash;
wenzelm [Tue, 23 Feb 2021 23:00:08 +0100] rev 73298
more on Isabelle_System.bash;
Tue, 23 Feb 2021 20:41:48 +0000 more specific name
haftmann [Tue, 23 Feb 2021 20:41:48 +0000] rev 73297
more specific name
Tue, 23 Feb 2021 20:41:48 +0000 more lemmas
haftmann [Tue, 23 Feb 2021 20:41:48 +0000] rev 73296
more lemmas
Tue, 23 Feb 2021 20:41:48 +0000 dropped obscure FIXME
haftmann [Tue, 23 Feb 2021 20:41:48 +0000] rev 73295
dropped obscure FIXME
Tue, 23 Feb 2021 12:20:50 +0100 proper usage of hypotheses for zipperposition's TPTP generation
desharna [Tue, 23 Feb 2021 12:20:50 +0100] rev 73294
proper usage of hypotheses for zipperposition's TPTP generation
Tue, 23 Feb 2021 10:13:09 +0100 merged
desharna [Tue, 23 Feb 2021 10:13:09 +0100] rev 73293
merged
Fri, 19 Feb 2021 11:52:34 +0100 tuned Mirabelle to parse option check_trivial only once
desharna [Fri, 19 Feb 2021 11:52:34 +0100] rev 73292
tuned Mirabelle to parse option check_trivial only once
Mon, 15 Feb 2021 08:36:19 +0100 merged
desharna [Mon, 15 Feb 2021 08:36:19 +0100] rev 73291
merged
Fri, 12 Feb 2021 11:21:44 +0100 merged
desharna [Fri, 12 Feb 2021 11:21:44 +0100] rev 73290
merged
Fri, 12 Feb 2021 11:18:44 +0100 added stride option to Mirabelle
desharna [Fri, 12 Feb 2021 11:18:44 +0100] rev 73289
added stride option to Mirabelle
Fri, 12 Feb 2021 11:18:12 +0100 proper prover capabilities for zipperposition
desharna [Fri, 12 Feb 2021 11:18:12 +0100] rev 73288
proper prover capabilities for zipperposition
Mon, 22 Feb 2021 23:31:59 +0100 NEWS;
wenzelm [Mon, 22 Feb 2021 23:31:59 +0100] rev 73287
NEWS;
Mon, 22 Feb 2021 22:41:50 +0100 merged
wenzelm [Mon, 22 Feb 2021 22:41:50 +0100] rev 73286
merged
Mon, 22 Feb 2021 22:06:41 +0100 clarified uses of Isabelle_System.bash_process: more checks, fewer messages;
wenzelm [Mon, 22 Feb 2021 22:06:41 +0100] rev 73285
clarified uses of Isabelle_System.bash_process: more checks, fewer messages;
Mon, 22 Feb 2021 18:19:38 +0100 tuned signature;
wenzelm [Mon, 22 Feb 2021 18:19:38 +0100] rev 73284
tuned signature;
Mon, 22 Feb 2021 18:16:56 +0100 more direct timing from bash_process wrapper;
wenzelm [Mon, 22 Feb 2021 18:16:56 +0100] rev 73283
more direct timing from bash_process wrapper;
Mon, 22 Feb 2021 17:19:05 +0100 tuned;
wenzelm [Mon, 22 Feb 2021 17:19:05 +0100] rev 73282
tuned;
Mon, 22 Feb 2021 17:17:30 +0100 clarified signature, following Isabelle/Scala;
wenzelm [Mon, 22 Feb 2021 17:17:30 +0100] rev 73281
clarified signature, following Isabelle/Scala;
Mon, 22 Feb 2021 16:58:56 +0100 tuned;
wenzelm [Mon, 22 Feb 2021 16:58:56 +0100] rev 73280
tuned;
Mon, 22 Feb 2021 16:54:33 +0100 clarified signature;
wenzelm [Mon, 22 Feb 2021 16:54:33 +0100] rev 73279
clarified signature;
Mon, 22 Feb 2021 16:45:41 +0100 clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;
wenzelm [Mon, 22 Feb 2021 16:45:41 +0100] rev 73278
clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;
Mon, 22 Feb 2021 15:24:04 +0100 clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm [Mon, 22 Feb 2021 15:24:04 +0100] rev 73277
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
Mon, 22 Feb 2021 15:20:45 +0100 tuned;
wenzelm [Mon, 22 Feb 2021 15:20:45 +0100] rev 73276
tuned;
Mon, 22 Feb 2021 14:48:03 +0100 clarified signature, following Isabelle/Scala;
wenzelm [Mon, 22 Feb 2021 14:48:03 +0100] rev 73275
clarified signature, following Isabelle/Scala;
Mon, 22 Feb 2021 13:29:55 +0100 tuned signature;
wenzelm [Mon, 22 Feb 2021 13:29:55 +0100] rev 73274
tuned signature;
Mon, 22 Feb 2021 12:30:05 +0100 clarified signature: process_result timing from Isabelle/Scala;
wenzelm [Mon, 22 Feb 2021 12:30:05 +0100] rev 73273
clarified signature: process_result timing from Isabelle/Scala;
Mon, 22 Feb 2021 18:28:12 +0000 NEWS
haftmann [Mon, 22 Feb 2021 18:28:12 +0000] rev 73272
NEWS
Mon, 22 Feb 2021 07:49:51 +0000 dedicated locale for preorder and abstract bdd operation
haftmann [Mon, 22 Feb 2021 07:49:51 +0000] rev 73271
dedicated locale for preorder and abstract bdd operation
Mon, 22 Feb 2021 07:49:48 +0000 get rid of traditional predicate
haftmann [Mon, 22 Feb 2021 07:49:48 +0000] rev 73270
get rid of traditional predicate
Sun, 21 Feb 2021 13:33:05 +0100 proper treatment of process_result;
wenzelm [Sun, 21 Feb 2021 13:33:05 +0100] rev 73269
proper treatment of process_result;
Sun, 21 Feb 2021 13:14:08 +0100 more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm [Sun, 21 Feb 2021 13:14:08 +0100] rev 73268
more accurate process_result in ML, corresponding to Process_Result in Scala;
Sun, 21 Feb 2021 12:24:40 +0100 clarified: proper trim_line for error;
wenzelm [Sun, 21 Feb 2021 12:24:40 +0100] rev 73267
clarified: proper trim_line for error;
Sun, 21 Feb 2021 11:53:05 +0100 unused;
wenzelm [Sun, 21 Feb 2021 11:53:05 +0100] rev 73266
unused;
Sun, 21 Feb 2021 00:49:09 +0100 clarified lines (again);
wenzelm [Sun, 21 Feb 2021 00:49:09 +0100] rev 73265
clarified lines (again);
Sat, 20 Feb 2021 23:01:35 +0100 clarified modules;
wenzelm [Sat, 20 Feb 2021 23:01:35 +0100] rev 73264
clarified modules;
Sat, 20 Feb 2021 22:09:16 +0100 more uniform Bash.process: always ask Isabelle/Scala;
wenzelm [Sat, 20 Feb 2021 22:09:16 +0100] rev 73263
more uniform Bash.process: always ask Isabelle/Scala;
Sat, 20 Feb 2021 21:38:23 +0100 more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process);
wenzelm [Sat, 20 Feb 2021 21:38:23 +0100] rev 73262
more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process);
Sat, 20 Feb 2021 20:23:30 +0100 clarified compiler options;
wenzelm [Sat, 20 Feb 2021 20:23:30 +0100] rev 73261
clarified compiler options;
Sat, 20 Feb 2021 20:10:09 +0100 tuned comments;
wenzelm [Sat, 20 Feb 2021 20:10:09 +0100] rev 73260
tuned comments;
Sat, 20 Feb 2021 17:28:56 +0100 removed obsolete RC tags;
wenzelm [Sat, 20 Feb 2021 17:28:56 +0100] rev 73259
removed obsolete RC tags;
Sat, 20 Feb 2021 17:21:48 +0100 more hints;
wenzelm [Sat, 20 Feb 2021 17:21:48 +0100] rev 73258
more hints;
Sat, 20 Feb 2021 17:04:26 +0100 merged
wenzelm [Sat, 20 Feb 2021 17:04:26 +0100] rev 73257
merged
Sat, 20 Feb 2021 13:49:24 +0100 Added tag Isabelle2021 for changeset 7e2a9a8c2b85
wenzelm [Sat, 20 Feb 2021 13:49:24 +0100] rev 73256
Added tag Isabelle2021 for changeset 7e2a9a8c2b85
Sat, 20 Feb 2021 13:42:37 +0100 provide naproche-755224402e36; Isabelle2021
wenzelm [Sat, 20 Feb 2021 13:42:37 +0100] rev 73255
provide naproche-755224402e36;
Fri, 19 Feb 2021 22:50:10 +0100 provide naproche-4ad61140062f;
wenzelm [Fri, 19 Feb 2021 22:50:10 +0100] rev 73254
provide naproche-4ad61140062f;
Fri, 19 Feb 2021 13:42:12 +0100 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de> [Fri, 19 Feb 2021 13:42:12 +0100] rev 73253
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Tue, 16 Feb 2021 17:12:02 +0000 tidied up a few ugly proofs
paulson <lp15@cam.ac.uk> [Tue, 16 Feb 2021 17:12:02 +0000] rev 73252
tidied up a few ugly proofs
Sun, 14 Feb 2021 20:13:13 +0100 merged
wenzelm [Sun, 14 Feb 2021 20:13:13 +0100] rev 73251
merged
Sun, 14 Feb 2021 17:32:06 +0100 provide naproche-6d0d76ce2f2a;
wenzelm [Sun, 14 Feb 2021 17:32:06 +0100] rev 73250
provide naproche-6d0d76ce2f2a;
Sun, 14 Feb 2021 15:40:38 +0100 Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b
wenzelm [Sun, 14 Feb 2021 15:40:38 +0100] rev 73249
Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b
Sat, 13 Feb 2021 21:19:53 +0100 updated to flatlaf-1.0;
wenzelm [Sat, 13 Feb 2021 21:19:53 +0100] rev 73248
updated to flatlaf-1.0;
Sat, 13 Feb 2021 20:39:29 +0100 tuned NEWS;
wenzelm [Sat, 13 Feb 2021 20:39:29 +0100] rev 73247
tuned NEWS;
Wed, 10 Feb 2021 22:30:51 +0100 tuned comments;
wenzelm [Wed, 10 Feb 2021 22:30:51 +0100] rev 73246
tuned comments;
Tue, 09 Feb 2021 15:40:23 +0100 more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
wenzelm [Tue, 09 Feb 2021 15:40:23 +0100] rev 73245
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
Tue, 09 Feb 2021 14:55:36 +0100 more parallelism: avoid exhaustion of standard thread pool;
wenzelm [Tue, 09 Feb 2021 14:55:36 +0100] rev 73244
more parallelism: avoid exhaustion of standard thread pool;
Fri, 12 Feb 2021 12:13:24 +0100 more robust: resolve historic components via current tool to access current server;
wenzelm [Fri, 12 Feb 2021 12:13:24 +0100] rev 73243
more robust: resolve historic components via current tool to access current server;
Fri, 12 Feb 2021 12:11:35 +0100 tuned signature;
wenzelm [Fri, 12 Feb 2021 12:11:35 +0100] rev 73242
tuned signature;
Thu, 11 Feb 2021 14:55:57 +0100 more parallelism;
wenzelm [Thu, 11 Feb 2021 14:55:57 +0100] rev 73241
more parallelism;
Tue, 09 Feb 2021 14:13:03 +0100 more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm [Tue, 09 Feb 2021 14:13:03 +0100] rev 73240
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
Tue, 09 Feb 2021 14:03:05 +0100 clarified signature;
wenzelm [Tue, 09 Feb 2021 14:03:05 +0100] rev 73239
clarified signature;
Mon, 08 Feb 2021 23:14:56 +0100 merged;
wenzelm [Mon, 08 Feb 2021 23:14:56 +0100] rev 73238
merged;
Mon, 08 Feb 2021 20:56:12 +0100 Added tag Isabelle2021-RC5 for changeset a88dbf2a020f
wenzelm [Mon, 08 Feb 2021 20:56:12 +0100] rev 73237
Added tag Isabelle2021-RC5 for changeset a88dbf2a020f
Mon, 08 Feb 2021 20:47:56 +0100 provide naproche-7d0947a91dd5;
wenzelm [Mon, 08 Feb 2021 20:47:56 +0100] rev 73236
provide naproche-7d0947a91dd5;
Sun, 07 Feb 2021 22:19:39 +0100 more complete solutions (amending 4d36070bdbf4);
wenzelm [Sun, 07 Feb 2021 22:19:39 +0100] rev 73235
more complete solutions (amending 4d36070bdbf4);
Sun, 07 Feb 2021 21:27:48 +0100 terminate faster (following dd9fc8a3036c);
wenzelm [Sun, 07 Feb 2021 21:27:48 +0100] rev 73234
terminate faster (following dd9fc8a3036c);
Sun, 07 Feb 2021 21:25:21 +0100 more robust: accommodate output lines produced by Scala "bash_process";
wenzelm [Sun, 07 Feb 2021 21:25:21 +0100] rev 73233
more robust: accommodate output lines produced by Scala "bash_process";
Sun, 07 Feb 2021 20:44:44 +0100 updated for release;
wenzelm [Sun, 07 Feb 2021 20:44:44 +0100] rev 73232
updated for release;
Sun, 07 Feb 2021 20:43:47 +0100 updated to flatlaf-1.0-rc3;
wenzelm [Sun, 07 Feb 2021 20:43:47 +0100] rev 73231
updated to flatlaf-1.0-rc3;
Sun, 07 Feb 2021 20:39:15 +0100 more robust: allow YXML text;
wenzelm [Sun, 07 Feb 2021 20:39:15 +0100] rev 73230
more robust: allow YXML text;
Sun, 07 Feb 2021 17:00:03 +0100 inherit ISABELLE_TMP from ML process, e.g. required for $AFP/Hello_World/RunningCodeFromIsabelle.thy;
wenzelm [Sun, 07 Feb 2021 17:00:03 +0100] rev 73229
inherit ISABELLE_TMP from ML process, e.g. required for $AFP/Hello_World/RunningCodeFromIsabelle.thy;
Sun, 07 Feb 2021 16:31:43 +0100 support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm [Sun, 07 Feb 2021 16:31:43 +0100] rev 73228
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
Sun, 07 Feb 2021 15:32:57 +0100 clarified modules: less redundancy;
wenzelm [Sun, 07 Feb 2021 15:32:57 +0100] rev 73227
clarified modules: less redundancy;
Sun, 07 Feb 2021 12:55:41 +0100 clarified modules: allow early invocation of Scala functions;
wenzelm [Sun, 07 Feb 2021 12:55:41 +0100] rev 73226
clarified modules: allow early invocation of Scala functions;
Sun, 07 Feb 2021 12:30:52 +0100 clarified modules: allow early definition of protocol commands;
wenzelm [Sun, 07 Feb 2021 12:30:52 +0100] rev 73225
clarified modules: allow early definition of protocol commands;
Wed, 03 Feb 2021 20:18:34 +0100 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm [Wed, 03 Feb 2021 20:18:34 +0100] rev 73224
clarified links to external files, e.g. .pdf within .thy source document;
Mon, 01 Feb 2021 18:12:44 +0100 avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
wenzelm [Mon, 01 Feb 2021 18:12:44 +0100] rev 73223
avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);
Mon, 01 Feb 2021 17:15:00 +0100 updated to flatlaf-1.0-rc2;
wenzelm [Mon, 01 Feb 2021 17:15:00 +0100] rev 73222
updated to flatlaf-1.0-rc2;
Mon, 08 Feb 2021 19:48:45 +0100 added lemmas
nipkow [Mon, 08 Feb 2021 19:48:45 +0100] rev 73221
added lemmas
Mon, 01 Feb 2021 16:03:07 +0100 merged
wenzelm [Mon, 01 Feb 2021 16:03:07 +0100] rev 73220
merged
Mon, 01 Feb 2021 14:01:01 +0100 updated for release;
wenzelm [Mon, 01 Feb 2021 14:01:01 +0100] rev 73219
updated for release;
Mon, 01 Feb 2021 13:50:41 +0100 Added tag Isabelle2021-RC4 for changeset 2ab14dbc6feb
wenzelm [Mon, 01 Feb 2021 13:50:41 +0100] rev 73218
Added tag Isabelle2021-RC4 for changeset 2ab14dbc6feb
Mon, 01 Feb 2021 13:29:22 +0100 provide naproche-20210201;
wenzelm [Mon, 01 Feb 2021 13:29:22 +0100] rev 73217
provide naproche-20210201;
Sun, 31 Jan 2021 20:44:42 +0100 clarified messages;
wenzelm [Sun, 31 Jan 2021 20:44:42 +0100] rev 73216
clarified messages;
Sun, 31 Jan 2021 20:39:16 +0100 more parallel;
wenzelm [Sun, 31 Jan 2021 20:39:16 +0100] rev 73215
more parallel;
Sun, 31 Jan 2021 19:46:40 +0100 more parallel;
wenzelm [Sun, 31 Jan 2021 19:46:40 +0100] rev 73214
more parallel;
Sun, 31 Jan 2021 12:10:20 +0100 contributors
Andreas Lochbihler <mail@andreas-lochbihler.de> [Sun, 31 Jan 2021 12:10:20 +0100] rev 73213
contributors
Sun, 31 Jan 2021 08:49:47 +0100 hide the internal abbreviations MR and MB
Andreas Lochbihler <mail@andreas-lochbihler.de> [Sun, 31 Jan 2021 08:49:47 +0100] rev 73212
hide the internal abbreviations MR and MB
Fri, 29 Jan 2021 13:06:29 +0100 optimize RBT_Impl
mraszyk [Fri, 29 Jan 2021 13:06:29 +0100] rev 73211
optimize RBT_Impl
Sat, 30 Jan 2021 21:43:13 +0100 merged
wenzelm [Sat, 30 Jan 2021 21:43:13 +0100] rev 73210
merged
Sat, 30 Jan 2021 20:47:00 +0100 more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
wenzelm [Sat, 30 Jan 2021 20:47:00 +0100] rev 73209
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);
Sat, 30 Jan 2021 19:36:42 +0100 tuned signature: more types;
wenzelm [Sat, 30 Jan 2021 19:36:42 +0100] rev 73208
tuned signature: more types;
Sat, 30 Jan 2021 19:33:14 +0100 clarified signature: proper order;
wenzelm [Sat, 30 Jan 2021 19:33:14 +0100] rev 73207
clarified signature: proper order;
Sat, 30 Jan 2021 19:29:22 +0100 clarified signature: more explicit types;
wenzelm [Sat, 30 Jan 2021 19:29:22 +0100] rev 73206
clarified signature: more explicit types;
Sat, 30 Jan 2021 18:58:56 +0100 tuned;
wenzelm [Sat, 30 Jan 2021 18:58:56 +0100] rev 73205
tuned;
Sat, 30 Jan 2021 18:34:37 +0100 clarified signature: no symbol markup within XML attributes;
wenzelm [Sat, 30 Jan 2021 18:34:37 +0100] rev 73204
clarified signature: no symbol markup within XML attributes;
Sat, 30 Jan 2021 17:15:14 +0100 clarified signature;
wenzelm [Sat, 30 Jan 2021 17:15:14 +0100] rev 73203
clarified signature;
(0) -30000 -10000 -3000 -1000 -480 tip