Sat, 28 Nov 2020 13:49:46 +0100 more robust (amending a4d7da18ac5c);
wenzelm [Sat, 28 Nov 2020 13:49:46 +0100] rev 72753
more robust (amending a4d7da18ac5c);
Sat, 28 Nov 2020 09:58:56 +0000 merged
paulson [Sat, 28 Nov 2020 09:58:56 +0000] rev 72752
merged
Fri, 27 Nov 2020 21:20:18 +0000 merged
paulson [Fri, 27 Nov 2020 21:20:18 +0000] rev 72751
merged
Fri, 27 Nov 2020 21:19:52 +0000 More removal of apply
paulson <lp15@cam.ac.uk> [Fri, 27 Nov 2020 21:19:52 +0000] rev 72750
More removal of apply
Fri, 27 Nov 2020 23:51:37 +0100 merged
wenzelm [Fri, 27 Nov 2020 23:51:37 +0100] rev 72749
merged
Fri, 27 Nov 2020 23:47:06 +0100 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm [Fri, 27 Nov 2020 23:47:06 +0100] rev 72748
more flexible syntax for theory load commands via Isabelle/Scala;
Fri, 27 Nov 2020 21:59:23 +0100 clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm [Fri, 27 Nov 2020 21:59:23 +0100] rev 72747
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically; propagate blob src_path from Scala to ML; clarified signature;
Fri, 27 Nov 2020 19:56:30 +0100 proper structural equality;
wenzelm [Fri, 27 Nov 2020 19:56:30 +0100] rev 72746
proper structural equality;
Fri, 27 Nov 2020 16:44:36 +0100 more explicit types;
wenzelm [Fri, 27 Nov 2020 16:44:36 +0100] rev 72745
more explicit types;
Fri, 27 Nov 2020 16:40:31 +0100 unused (see 7634d33c1a79);
wenzelm [Fri, 27 Nov 2020 16:40:31 +0100] rev 72744
unused (see 7634d33c1a79);
Fri, 27 Nov 2020 14:25:39 +0100 clarified signature;
wenzelm [Fri, 27 Nov 2020 14:25:39 +0100] rev 72743
clarified signature;
Fri, 27 Nov 2020 14:00:54 +0100 clarified modules;
wenzelm [Fri, 27 Nov 2020 14:00:54 +0100] rev 72742
clarified modules;
Fri, 27 Nov 2020 11:50:23 +0100 clarified file names;
wenzelm [Fri, 27 Nov 2020 11:50:23 +0100] rev 72741
clarified file names;
Fri, 27 Nov 2020 11:41:43 +0100 tuned signature;
wenzelm [Fri, 27 Nov 2020 11:41:43 +0100] rev 72740
tuned signature;
Fri, 27 Nov 2020 06:48:35 +0000 refined syntax for bundle mixins for locale and class specifications
haftmann [Fri, 27 Nov 2020 06:48:35 +0000] rev 72739
refined syntax for bundle mixins for locale and class specifications
Thu, 26 Nov 2020 23:23:19 +0100 store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm [Thu, 26 Nov 2020 23:23:19 +0100] rev 72738
store timings for used_theories in canonical order, with reconstructed store.read_theories;
Thu, 26 Nov 2020 20:49:40 +0000 merged
paulson [Thu, 26 Nov 2020 20:49:40 +0000] rev 72737
merged
Thu, 26 Nov 2020 18:09:15 +0000 merged
paulson [Thu, 26 Nov 2020 18:09:15 +0000] rev 72736
merged
Thu, 26 Nov 2020 18:09:02 +0000 Stepan Holub's stronger version of comm_append_are_replicate, and a de-applied Word.thy
paulson <lp15@cam.ac.uk> [Thu, 26 Nov 2020 18:09:02 +0000] rev 72735
Stepan Holub's stronger version of comm_append_are_replicate, and a de-applied Word.thy
Thu, 26 Nov 2020 19:27:42 +0100 merged
nipkow [Thu, 26 Nov 2020 19:27:42 +0100] rev 72734
merged
Thu, 26 Nov 2020 19:27:28 +0100 tuned
nipkow [Thu, 26 Nov 2020 19:27:28 +0100] rev 72733
tuned
Thu, 26 Nov 2020 14:53:38 +0100 removed assumptions in lemma (Stepan Holub)
nipkow [Thu, 26 Nov 2020 14:53:38 +0100] rev 72732
removed assumptions in lemma (Stepan Holub)
Thu, 26 Nov 2020 18:32:06 +0100 merged
wenzelm [Thu, 26 Nov 2020 18:32:06 +0100] rev 72731
merged
Thu, 26 Nov 2020 18:05:24 +0100 more exports from rendering;
wenzelm [Thu, 26 Nov 2020 18:05:24 +0100] rev 72730
more exports from rendering; suppress empty exports;
Thu, 26 Nov 2020 17:32:43 +0100 clarified signature;
wenzelm [Thu, 26 Nov 2020 17:32:43 +0100] rev 72729
clarified signature;
Thu, 26 Nov 2020 17:23:33 +0100 clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm [Thu, 26 Nov 2020 17:23:33 +0100] rev 72728
clarified options: batch-build has pide_reports disabled by default (requires significant resources);
Thu, 26 Nov 2020 17:01:19 +0100 tuned;
wenzelm [Thu, 26 Nov 2020 17:01:19 +0100] rev 72727
tuned;
Thu, 26 Nov 2020 16:51:40 +0100 proper return code for more errors (amending d892f6d66402);
wenzelm [Thu, 26 Nov 2020 16:51:40 +0100] rev 72726
proper return code for more errors (amending d892f6d66402);
Thu, 26 Nov 2020 16:19:55 +0100 more exports, as in "isabelle dump";
wenzelm [Thu, 26 Nov 2020 16:19:55 +0100] rev 72725
more exports, as in "isabelle dump";
Thu, 26 Nov 2020 16:14:16 +0100 tuned;
wenzelm [Thu, 26 Nov 2020 16:14:16 +0100] rev 72724
tuned;
Thu, 26 Nov 2020 16:08:39 +0100 clarified signature;
wenzelm [Thu, 26 Nov 2020 16:08:39 +0100] rev 72723
clarified signature;
Thu, 26 Nov 2020 15:59:09 +0100 clarified signature: initial markup is_empty, not init_markup;
wenzelm [Thu, 26 Nov 2020 15:59:09 +0100] rev 72722
clarified signature: initial markup is_empty, not init_markup;
Thu, 26 Nov 2020 15:49:27 +0100 clarified signature: prefer high-level Snapshot over low-level Command.State;
wenzelm [Thu, 26 Nov 2020 15:49:27 +0100] rev 72721
clarified signature: prefer high-level Snapshot over low-level Command.State;
Thu, 26 Nov 2020 15:18:09 +0100 tuned;
wenzelm [Thu, 26 Nov 2020 15:18:09 +0100] rev 72720
tuned;
Thu, 26 Nov 2020 15:16:37 +0100 more strict;
wenzelm [Thu, 26 Nov 2020 15:16:37 +0100] rev 72719
more strict;
Thu, 26 Nov 2020 14:48:22 +0100 clarified signature;
wenzelm [Thu, 26 Nov 2020 14:48:22 +0100] rev 72718
clarified signature;
Thu, 26 Nov 2020 13:15:57 +0100 tuned;
wenzelm [Thu, 26 Nov 2020 13:15:57 +0100] rev 72717
tuned;
Thu, 26 Nov 2020 12:27:09 +0100 clarified signature;
wenzelm [Thu, 26 Nov 2020 12:27:09 +0100] rev 72716
clarified signature;
Thu, 26 Nov 2020 12:21:45 +0100 clarified signature --- avoid repeated open_database on server;
wenzelm [Thu, 26 Nov 2020 12:21:45 +0100] rev 72715
clarified signature --- avoid repeated open_database on server;
Thu, 26 Nov 2020 15:51:20 +0000 renaming
Peter Lammich [Thu, 26 Nov 2020 15:51:20 +0000] rev 72714
renaming
Wed, 25 Nov 2020 21:13:45 +0100 merged
wenzelm [Wed, 25 Nov 2020 21:13:45 +0100] rev 72713
merged
Wed, 25 Nov 2020 21:08:43 +0100 recovered document output from 6bc199a70bf9;
wenzelm [Wed, 25 Nov 2020 21:08:43 +0100] rev 72712
recovered document output from 6bc199a70bf9;
Wed, 25 Nov 2020 20:48:33 +0100 clarified command_timings protocol;
wenzelm [Wed, 25 Nov 2020 20:48:33 +0100] rev 72711
clarified command_timings protocol;
Wed, 25 Nov 2020 17:49:09 +0100 more robust: include reports from Thy_Output.present_thy/output_document;
wenzelm [Wed, 25 Nov 2020 17:49:09 +0100] rev 72710
more robust: include reports from Thy_Output.present_thy/output_document;
Wed, 25 Nov 2020 16:14:16 +0100 more complete report positions, notably for command 'back' (amending eca176f773e0);
wenzelm [Wed, 25 Nov 2020 16:14:16 +0100] rev 72709
more complete report positions, notably for command 'back' (amending eca176f773e0);
Wed, 25 Nov 2020 15:24:55 +0100 tuned signature;
wenzelm [Wed, 25 Nov 2020 15:24:55 +0100] rev 72708
tuned signature;
Wed, 25 Nov 2020 15:12:02 +0100 clarified signature;
wenzelm [Wed, 25 Nov 2020 15:12:02 +0100] rev 72707
clarified signature;
Wed, 25 Nov 2020 13:51:28 +0100 unused;
wenzelm [Wed, 25 Nov 2020 13:51:28 +0100] rev 72706
unused;
Wed, 25 Nov 2020 13:30:06 +0100 unused;
wenzelm [Wed, 25 Nov 2020 13:30:06 +0100] rev 72705
unused;
Wed, 25 Nov 2020 13:22:34 +0100 tuned;
wenzelm [Wed, 25 Nov 2020 13:22:34 +0100] rev 72704
tuned;
Wed, 25 Nov 2020 13:12:31 +0100 removed pointless case: messages should always carry proper position;
wenzelm [Wed, 25 Nov 2020 13:12:31 +0100] rev 72703
removed pointless case: messages should always carry proper position;
Wed, 25 Nov 2020 13:06:03 +0100 clarified names;
wenzelm [Wed, 25 Nov 2020 13:06:03 +0100] rev 72702
clarified names;
Wed, 25 Nov 2020 12:57:45 +0100 eliminated pointless transaction;
wenzelm [Wed, 25 Nov 2020 12:57:45 +0100] rev 72701
eliminated pointless transaction;
Wed, 25 Nov 2020 12:55:09 +0100 tuned signature;
wenzelm [Wed, 25 Nov 2020 12:55:09 +0100] rev 72700
tuned signature;
Wed, 25 Nov 2020 12:52:00 +0100 clarified document_output vs. progress;
wenzelm [Wed, 25 Nov 2020 12:52:00 +0100] rev 72699
clarified document_output vs. progress;
Wed, 25 Nov 2020 12:34:08 +0100 clarified: more uniform;
wenzelm [Wed, 25 Nov 2020 12:34:08 +0100] rev 72698
clarified: more uniform;
Tue, 24 Nov 2020 16:49:42 +0100 more robust;
wenzelm [Tue, 24 Nov 2020 16:49:42 +0100] rev 72697
more robust;
Tue, 24 Nov 2020 16:39:58 +0100 clarified signature and database layout;
wenzelm [Tue, 24 Nov 2020 16:39:58 +0100] rev 72696
clarified signature and database layout;
Mon, 23 Nov 2020 16:18:22 +0100 clarified messages;
wenzelm [Mon, 23 Nov 2020 16:18:22 +0100] rev 72695
clarified messages;
Mon, 23 Nov 2020 16:02:04 +0100 unused (see ac7ae5067783, 1c451e5c145f);
wenzelm [Mon, 23 Nov 2020 16:02:04 +0100] rev 72694
unused (see ac7ae5067783, 1c451e5c145f);
Mon, 23 Nov 2020 15:34:35 +0100 unused;
wenzelm [Mon, 23 Nov 2020 15:34:35 +0100] rev 72693
unused;
Mon, 23 Nov 2020 15:14:58 +0100 support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm [Mon, 23 Nov 2020 15:14:58 +0100] rev 72692
support for PIDE markup in batch build (inactive due to pide_reports=false);
Mon, 23 Nov 2020 13:52:14 +0100 clarified signature;
wenzelm [Mon, 23 Nov 2020 13:52:14 +0100] rev 72691
clarified signature;
Mon, 23 Nov 2020 13:37:10 +0100 proper output of document sources (cf. d892f6d66402);
wenzelm [Mon, 23 Nov 2020 13:37:10 +0100] rev 72690
proper output of document sources (cf. d892f6d66402);
Tue, 24 Nov 2020 19:49:59 +0100 proper parsing of TSTP HOL lines
desharna [Tue, 24 Nov 2020 19:49:59 +0100] rev 72689
proper parsing of TSTP HOL lines
Mon, 23 Nov 2020 19:57:55 +0100 proper defn of a heap
nipkow [Mon, 23 Nov 2020 19:57:55 +0100] rev 72688
proper defn of a heap
Sun, 22 Nov 2020 18:26:54 +0000 merged
paulson [Sun, 22 Nov 2020 18:26:54 +0000] rev 72687
merged
Sun, 22 Nov 2020 18:26:45 +0000 cleanup of old proofs
paulson <lp15@cam.ac.uk> [Sun, 22 Nov 2020 18:26:45 +0000] rev 72686
cleanup of old proofs
Sun, 22 Nov 2020 13:31:33 +0100 proper output directory (amending cc1347c8c804);
wenzelm [Sun, 22 Nov 2020 13:31:33 +0100] rev 72685
proper output directory (amending cc1347c8c804);
Sun, 22 Nov 2020 13:11:40 +0100 updated to cvc4-1.8;
wenzelm [Sun, 22 Nov 2020 13:11:40 +0100] rev 72684
updated to cvc4-1.8;
Sat, 21 Nov 2020 21:02:38 +0100 clarified signature: prefer Database_Context;
wenzelm [Sat, 21 Nov 2020 21:02:38 +0100] rev 72683
clarified signature: prefer Database_Context;
Sat, 21 Nov 2020 20:35:48 +0100 clarified modules;
wenzelm [Sat, 21 Nov 2020 20:35:48 +0100] rev 72682
clarified modules;
Sat, 21 Nov 2020 19:48:05 +0100 tuned NEWS;
wenzelm [Sat, 21 Nov 2020 19:48:05 +0100] rev 72681
tuned NEWS;
Sat, 21 Nov 2020 18:44:38 +0100 removed unused material;
wenzelm [Sat, 21 Nov 2020 18:44:38 +0100] rev 72680
removed unused material;
Sat, 21 Nov 2020 18:16:25 +0100 more NEWS;
wenzelm [Sat, 21 Nov 2020 18:16:25 +0100] rev 72679
more NEWS;
Sat, 21 Nov 2020 17:58:00 +0100 NEWS;
wenzelm [Sat, 21 Nov 2020 17:58:00 +0100] rev 72678
NEWS;
Sat, 21 Nov 2020 17:57:54 +0100 more interrupts;
wenzelm [Sat, 21 Nov 2020 17:57:54 +0100] rev 72677
more interrupts;
Sat, 21 Nov 2020 17:30:44 +0100 clarified messages;
wenzelm [Sat, 21 Nov 2020 17:30:44 +0100] rev 72676
clarified messages;
Sat, 21 Nov 2020 17:12:17 +0100 clarified document output;
wenzelm [Sat, 21 Nov 2020 17:12:17 +0100] rev 72675
clarified document output;
Sat, 21 Nov 2020 16:22:35 +0100 clarified messages;
wenzelm [Sat, 21 Nov 2020 16:22:35 +0100] rev 72674
clarified messages;
Sat, 21 Nov 2020 16:07:20 +0100 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm [Sat, 21 Nov 2020 16:07:20 +0100] rev 72673
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
Sat, 21 Nov 2020 15:20:12 +0100 tuned signature;
wenzelm [Sat, 21 Nov 2020 15:20:12 +0100] rev 72672
tuned signature;
Sat, 21 Nov 2020 00:29:41 +0100 more standard imports;
wenzelm [Sat, 21 Nov 2020 00:29:41 +0100] rev 72671
more standard imports;
Fri, 20 Nov 2020 23:53:37 +0100 tuned signature;
wenzelm [Fri, 20 Nov 2020 23:53:37 +0100] rev 72670
tuned signature;
Fri, 20 Nov 2020 23:47:34 +0100 generate theory HTML in Isabelle/Scala;
wenzelm [Fri, 20 Nov 2020 23:47:34 +0100] rev 72669
generate theory HTML in Isabelle/Scala; discontinued HTML support in Isabelle/ML;
Fri, 20 Nov 2020 14:29:21 +0100 merged
desharna [Fri, 20 Nov 2020 14:29:21 +0100] rev 72668
merged
Fri, 13 Nov 2020 09:47:59 +0100 Add support for CVC4 1.8 to Sledgehammer
desharna [Fri, 13 Nov 2020 09:47:59 +0100] rev 72667
Add support for CVC4 1.8 to Sledgehammer
Fri, 20 Nov 2020 12:00:08 +0100 proper meta_digest: avoid non-portable position information;
wenzelm [Fri, 20 Nov 2020 12:00:08 +0100] rev 72666
proper meta_digest: avoid non-portable position information;
Thu, 19 Nov 2020 22:05:34 +0100 clarified messages;
wenzelm [Thu, 19 Nov 2020 22:05:34 +0100] rev 72665
clarified messages;
Thu, 19 Nov 2020 21:59:17 +0100 proper message;
wenzelm [Thu, 19 Nov 2020 21:59:17 +0100] rev 72664
proper message;
Thu, 19 Nov 2020 21:23:12 +0100 clarified signature;
wenzelm [Thu, 19 Nov 2020 21:23:12 +0100] rev 72663
clarified signature;
Thu, 19 Nov 2020 21:12:35 +0100 clarified modules;
wenzelm [Thu, 19 Nov 2020 21:12:35 +0100] rev 72662
clarified modules;
Thu, 19 Nov 2020 17:50:14 +0100 more robust library_call (again): dynamic file name, static symbol;
wenzelm [Thu, 19 Nov 2020 17:50:14 +0100] rev 72661
more robust library_call (again): dynamic file name, static symbol;
Thu, 19 Nov 2020 17:46:58 +0100 updated to polyml-test-7e49fce62e3d --- follow current ongoing development;
wenzelm [Thu, 19 Nov 2020 17:46:58 +0100] rev 72660
updated to polyml-test-7e49fce62e3d --- follow current ongoing development;
Thu, 19 Nov 2020 15:11:37 +0100 reintroduced and renamed THF_Predicate_Free deleted by c7e2a9bdc585
desharna [Thu, 19 Nov 2020 15:11:37 +0100] rev 72659
reintroduced and renamed THF_Predicate_Free deleted by c7e2a9bdc585
Thu, 19 Nov 2020 14:46:49 +0100 repaired thf output broken by c7e2a9bdc585
desharna [Thu, 19 Nov 2020 14:46:49 +0100] rev 72658
repaired thf output broken by c7e2a9bdc585
Thu, 19 Nov 2020 14:43:50 +0100 renamed data type
desharna [Thu, 19 Nov 2020 14:43:50 +0100] rev 72657
renamed data type
Thu, 19 Nov 2020 10:11:11 +0100 tuned terminology
nipkow [Thu, 19 Nov 2020 10:11:11 +0100] rev 72656
tuned terminology
Wed, 18 Nov 2020 21:53:58 +0100 merged
wenzelm [Wed, 18 Nov 2020 21:53:58 +0100] rev 72655
merged
Wed, 18 Nov 2020 21:39:55 +0100 tuned signature;
wenzelm [Wed, 18 Nov 2020 21:39:55 +0100] rev 72654
tuned signature;
Wed, 18 Nov 2020 21:34:13 +0100 store documents within session database, instead of browser_info directory;
wenzelm [Wed, 18 Nov 2020 21:34:13 +0100] rev 72653
store documents within session database, instead of browser_info directory;
Wed, 18 Nov 2020 15:52:12 +0100 clarified modules;
wenzelm [Wed, 18 Nov 2020 15:52:12 +0100] rev 72652
clarified modules;
Wed, 18 Nov 2020 15:47:53 +0100 clarified modules;
wenzelm [Wed, 18 Nov 2020 15:47:53 +0100] rev 72651
clarified modules;
Wed, 18 Nov 2020 15:41:02 +0100 more robust: ensure coherence wrt. build database;
wenzelm [Wed, 18 Nov 2020 15:41:02 +0100] rev 72650
more robust: ensure coherence wrt. build database;
Wed, 18 Nov 2020 15:36:41 +0100 clarified signature: more explicit types;
wenzelm [Wed, 18 Nov 2020 15:36:41 +0100] rev 72649
clarified signature: more explicit types;
Wed, 18 Nov 2020 13:16:08 +0100 more explicit presentation directory;
wenzelm [Wed, 18 Nov 2020 13:16:08 +0100] rev 72648
more explicit presentation directory;
Wed, 18 Nov 2020 13:14:01 +0100 more robust, e.g. for "isabelle build_doc system";
wenzelm [Wed, 18 Nov 2020 13:14:01 +0100] rev 72647
more robust, e.g. for "isabelle build_doc system";
Wed, 18 Nov 2020 08:10:40 +0100 tuned;
wenzelm [Wed, 18 Nov 2020 08:10:40 +0100] rev 72646
tuned;
Wed, 18 Nov 2020 18:45:50 +0000 merged
paulson [Wed, 18 Nov 2020 18:45:50 +0000] rev 72645
merged
Wed, 18 Nov 2020 16:35:20 +0000 merged
paulson [Wed, 18 Nov 2020 16:35:20 +0000] rev 72644
merged
Wed, 18 Nov 2020 16:35:14 +0000 de-applying
paulson <lp15@cam.ac.uk> [Wed, 18 Nov 2020 16:35:14 +0000] rev 72643
de-applying
Wed, 18 Nov 2020 19:38:19 +0100 new theory
nipkow [Wed, 18 Nov 2020 19:38:19 +0100] rev 72642
new theory
Wed, 18 Nov 2020 13:44:34 +0100 Tuned parentheses in TPTP output
desharna [Wed, 18 Nov 2020 13:44:34 +0100] rev 72641
Tuned parentheses in TPTP output
Tue, 17 Nov 2020 23:26:41 +0100 simplified/clarified persistent session information;
wenzelm [Tue, 17 Nov 2020 23:26:41 +0100] rev 72640
simplified/clarified persistent session information;
Tue, 17 Nov 2020 22:58:55 +0100 merged
wenzelm [Tue, 17 Nov 2020 22:58:55 +0100] rev 72639
merged
Tue, 17 Nov 2020 22:57:56 +0100 refer to command_timings/last_timing via resources;
wenzelm [Tue, 17 Nov 2020 22:57:56 +0100] rev 72638
refer to command_timings/last_timing via resources;
Tue, 17 Nov 2020 22:05:59 +0100 more uniform Resources.init_session via YXML;
wenzelm [Tue, 17 Nov 2020 22:05:59 +0100] rev 72637
more uniform Resources.init_session via YXML;
Tue, 17 Nov 2020 16:54:49 +0100 proper link for Pure;
wenzelm [Tue, 17 Nov 2020 16:54:49 +0100] rev 72636
proper link for Pure;
Tue, 17 Nov 2020 16:48:18 +0100 proper link location;
wenzelm [Tue, 17 Nov 2020 16:48:18 +0100] rev 72635
proper link location;
Tue, 17 Nov 2020 16:34:01 +0100 clarified access to single database server vs. collection of database files;
wenzelm [Tue, 17 Nov 2020 16:34:01 +0100] rev 72634
clarified access to single database server vs. collection of database files;
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 tip