Fri, 17 Jul 2020 20:35:43 +0200 wenzelm clarified -- avoid non-standard extend/merge;
Fri, 17 Jul 2020 20:22:58 +0200 wenzelm tuned -- avoid non-standard extend;
Fri, 17 Jul 2020 19:10:24 +0200 wenzelm clarified -- avoid non-standard extend/merge;
Fri, 17 Jul 2020 17:06:54 +0200 wenzelm proper session imports;
Fri, 17 Jul 2020 15:13:03 +0200 wenzelm clarified -- avoid non-standard extend;
Fri, 17 Jul 2020 15:08:56 +0200 wenzelm tuned -- avoid non-standard extend/merge;
Fri, 17 Jul 2020 14:56:55 +0200 wenzelm prefer conservative extend/merge of theory naming;
Thu, 16 Jul 2020 22:24:03 +0200 wenzelm support native PID for ML process;
Thu, 16 Jul 2020 20:35:03 +0200 wenzelm merged
Thu, 16 Jul 2020 20:34:21 +0200 wenzelm clarified theory data: more robust merge;
Thu, 16 Jul 2020 16:53:08 +0200 wenzelm proper import sessions;
Thu, 16 Jul 2020 16:48:12 +0200 wenzelm more thorough extend/merge (for Theory.join_theory);
Thu, 16 Jul 2020 16:38:25 +0200 wenzelm more thorough extend/merge (for Theory.join_theory);
Thu, 16 Jul 2020 16:00:52 +0200 wenzelm more thorough extend/merge (for Theory.join_theory);
Thu, 16 Jul 2020 14:36:43 +0200 wenzelm more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);
Thu, 16 Jul 2020 11:43:32 +0200 wenzelm more robust: avoid potential problems with encoding of directory name;
Thu, 16 Jul 2020 04:52:26 +0000 haftmann tuned grouping
Thu, 16 Jul 2020 04:52:25 +0000 haftmann yet another alias
Wed, 15 Jul 2020 20:06:45 +0200 wenzelm more robust wrt. experimental changes in Poly/ML;
Wed, 15 Jul 2020 17:10:26 +0200 wenzelm more robust: handle unavailable statistics;
Wed, 15 Jul 2020 16:28:26 +0200 wenzelm merged
Wed, 15 Jul 2020 16:10:43 +0200 wenzelm clarified user counters: expose tasks to external monitor;
Wed, 15 Jul 2020 12:43:36 +0200 wenzelm proper platform path for Windows;
Wed, 15 Jul 2020 12:30:25 +0200 wenzelm clarified signature;
Wed, 15 Jul 2020 12:04:48 +0200 wenzelm support for monitoring of external ML process;
Wed, 15 Jul 2020 11:56:43 +0200 wenzelm clarified signature;
Mon, 13 Jul 2020 23:23:35 +0200 wenzelm more robust;
Mon, 13 Jul 2020 23:10:47 +0200 wenzelm support for monitoring of external ML process;
Mon, 13 Jul 2020 22:07:18 +0200 wenzelm clarified modules: ML_Statistics within bootstrap environment;
Mon, 13 Jul 2020 21:20:36 +0200 wenzelm misc tuning and modernization;
Mon, 13 Jul 2020 17:08:45 +0200 wenzelm clarified examples;
Mon, 13 Jul 2020 15:23:32 +0000 haftmann concatentation of bit values
Sun, 12 Jul 2020 18:10:06 +0000 haftmann prefer canonically oriented lists of bits and more direct characterizations in definitions
Sun, 12 Jul 2020 18:10:06 +0000 haftmann more simp rules for concrete numerical values
Sun, 12 Jul 2020 18:10:06 +0000 haftmann words added to code generator test
Sat, 11 Jul 2020 18:09:09 +0000 haftmann a generic horner sum operation
Sat, 11 Jul 2020 18:09:08 +0000 haftmann more thms
Sat, 11 Jul 2020 18:19:08 +0200 wenzelm clarified message --- as in former ML version (see 940195fbb282);
Sat, 11 Jul 2020 17:15:28 +0200 wenzelm clarified signature;
Sat, 11 Jul 2020 17:08:26 +0200 wenzelm clarified messages: avoid duplicate Timing;
Sat, 11 Jul 2020 16:58:38 +0200 wenzelm clarified messages;
Sat, 11 Jul 2020 16:41:55 +0200 wenzelm clarified signature;
Sat, 11 Jul 2020 16:37:32 +0200 wenzelm tuned;
Sat, 11 Jul 2020 16:32:25 +0200 wenzelm avoid duplicate Timing messages (see also 5c4800f6b25a);
Sat, 11 Jul 2020 16:25:17 +0200 wenzelm more accurate message;
Sat, 11 Jul 2020 15:52:54 +0200 wenzelm tuned;
Sat, 11 Jul 2020 15:51:15 +0200 wenzelm clarified signature;
Sat, 11 Jul 2020 15:23:22 +0200 wenzelm clarified inlined protocol messages;
Sat, 11 Jul 2020 14:44:50 +0200 wenzelm removed unused property;
Sat, 11 Jul 2020 06:21:04 +0000 haftmann signed_take_bit
Sat, 11 Jul 2020 06:21:02 +0000 haftmann more on single-bit operations
Fri, 10 Jul 2020 22:38:03 +0200 wenzelm proper session Timing for build_history log file (see 5c4800f6b25a);
Fri, 10 Jul 2020 21:58:49 +0200 wenzelm clarified signature;
Fri, 10 Jul 2020 21:30:21 +0200 wenzelm more robust, notably for isabelle_cronjob;
Fri, 10 Jul 2020 21:23:01 +0200 wenzelm more robust build_session protocol: allow prover process to terminate/crash without build_session_finished message;
Thu, 09 Jul 2020 11:39:16 +0200 desharna Update Metis to 2.4
Wed, 08 Jul 2020 16:35:23 +0200 wenzelm updated to polyml-5.8.1-20200708: recent repository version for testing;
Wed, 08 Jul 2020 14:43:02 +0200 wenzelm more robust protocol for "Timing ..." messages, notably for pide_session=true;
Mon, 06 Jul 2020 16:52:48 +0200 blanchet removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible with post-2016 reforms to local theories
Mon, 06 Jul 2020 10:47:30 +0000 haftmann separation of traditional bit operations
Sun, 05 Jul 2020 11:06:09 +0200 wenzelm no pide_session on macos: avoid odd "hang" of remote_build_history;
Sun, 05 Jul 2020 11:00:57 +0200 wenzelm support generated preferences, i.e. non-strict system options;
Sat, 04 Jul 2020 20:45:24 +0000 haftmann factored out auxiliary theory
Sat, 04 Jul 2020 20:45:21 +0000 haftmann prefer explicit proof
Fri, 03 Jul 2020 17:11:57 +0200 wenzelm tuned whitespace;
Fri, 03 Jul 2020 17:11:26 +0200 wenzelm use less memory on old hardware;
Fri, 03 Jul 2020 17:00:41 +0200 wenzelm clarified signature;
Fri, 03 Jul 2020 16:48:57 +0200 wenzelm clarified log message (more uniform);
Fri, 03 Jul 2020 06:18:29 +0000 haftmann misc lemma tuning
Fri, 03 Jul 2020 06:18:27 +0000 haftmann explicit proofs for bit projections
Thu, 02 Jul 2020 12:10:58 +0000 haftmann extraction of equations x = t from premises beneath meta-all
Thu, 02 Jul 2020 08:49:04 +0000 haftmann a small aggiornamento for Z2
Thu, 02 Jul 2020 08:49:03 +0000 haftmann removed superfluous dependency
Wed, 01 Jul 2020 17:32:11 +0000 haftmann factored out ancient numeral representation
Wed, 01 Jul 2020 17:32:11 +0000 haftmann moved to Word_Lib
Wed, 01 Jul 2020 17:32:10 +0000 haftmann more explicit proofs
Wed, 01 Jul 2020 22:11:30 +0200 wenzelm clarified options --- potentially more robust;
Wed, 01 Jul 2020 21:14:04 +0200 wenzelm tuned message;
Sat, 27 Jun 2020 11:25:30 +0200 wenzelm clarified signature;
Fri, 26 Jun 2020 17:34:34 +0200 wenzelm more CONTRIBUTORS;
Thu, 25 Jun 2020 15:45:15 +0200 wenzelm more uniform URL (see 60b5a4731695);
Wed, 24 Jun 2020 20:59:50 +0200 wenzelm clarified use of memory: prefer share tree structures over fresh strings;
Wed, 24 Jun 2020 11:16:57 +0200 wenzelm more Java heap space (see 2d658beb815b);
Sun, 21 Jun 2020 11:12:19 +0200 wenzelm clarified NEWS;
Sat, 20 Jun 2020 22:35:24 +0200 wenzelm enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);
Sat, 20 Jun 2020 21:44:43 +0200 wenzelm discontinued old AFP test: ancient hardware with insufficient resources;
Sat, 20 Jun 2020 19:05:56 +0200 wenzelm tuned output;
Sat, 20 Jun 2020 16:36:32 +0200 wenzelm merged
Sat, 20 Jun 2020 16:18:33 +0200 wenzelm share cache for parallel sessions;
Sat, 20 Jun 2020 15:09:20 +0200 wenzelm clarified signature;
Sat, 20 Jun 2020 14:36:27 +0200 wenzelm more caching, notably for build/pide_session;
Sat, 20 Jun 2020 11:01:57 +0200 wenzelm removed pointless pide_exports: unused during "build_session" process (reverting 6a64205b491a);
Fri, 19 Jun 2020 20:15:00 +0200 wenzelm tuned --- avoid error in IntelliJ IDEA;
Sat, 20 Jun 2020 05:56:28 +0000 haftmann simp rules for conversions
Sat, 20 Jun 2020 05:56:28 +0000 haftmann more class operations for the sake of efficient generated code
Fri, 19 Jun 2020 18:44:36 +0200 wenzelm merged
Fri, 19 Jun 2020 18:44:31 +0200 wenzelm back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);
Fri, 19 Jun 2020 18:29:37 +0200 wenzelm back to pide_session=false for now, requires too many JVM resources (reverting 026de3424c39);
Fri, 19 Jun 2020 18:22:03 +0200 wenzelm clarified signature;
Fri, 19 Jun 2020 16:12:32 +0200 wenzelm avoid redundant export handling for build;
Fri, 19 Jun 2020 09:46:47 +0000 haftmann prefer single name
Thu, 18 Jun 2020 09:07:54 +0000 haftmann more lemmas
Thu, 18 Jun 2020 09:07:30 +0000 haftmann build bit operations on word on library theory on bit operations
Thu, 18 Jun 2020 09:07:30 +0000 haftmann bit operations as distinctive library theory
Thu, 18 Jun 2020 09:07:30 +0000 haftmann tweak for code generation
Thu, 18 Jun 2020 09:07:30 +0000 haftmann pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
Thu, 18 Jun 2020 09:07:30 +0000 haftmann more lemmas and less name space pollution
Thu, 18 Jun 2020 09:07:30 +0000 haftmann canonical bit shifts for word type, leaving duplicates as they are at the moment
Thu, 18 Jun 2020 09:07:30 +0000 haftmann essential instance about bit structure
Thu, 18 Jun 2020 09:07:29 +0000 haftmann more transfer rules
Thu, 18 Jun 2020 09:07:29 +0000 haftmann dropped yet another duplicate
Thu, 18 Jun 2020 09:07:29 +0000 haftmann fundamental construction of word type following existing transfer rules
Thu, 18 Jun 2020 09:07:29 +0000 haftmann replaced mere alias by input abbreviation
Thu, 18 Jun 2020 09:07:29 +0000 haftmann replaced mere alias by abbreviation
Thu, 18 Jun 2020 09:07:29 +0000 haftmann replaced operation with weak abstraction by input abbreviation
Thu, 18 Jun 2020 09:07:29 +0000 haftmann avoid compound operation
Thu, 18 Jun 2020 09:07:29 +0000 haftmann formal relationships between operations
Thu, 18 Jun 2020 09:07:29 +0000 haftmann eliminated warnings
Thu, 18 Jun 2020 09:07:28 +0000 haftmann replaced mere alias by input abbreviation
Wed, 17 Jun 2020 20:42:52 +0200 wenzelm enable pide_session by default;
Wed, 17 Jun 2020 19:46:50 +0200 wenzelm avoid resource problems of JVM by too many parallel XZ compression tasks;
Tue, 16 Jun 2020 08:41:39 +0000 haftmann interpretations for boolean operators
Tue, 16 Jun 2020 08:41:39 +0000 haftmann more specific thm reference
Sat, 13 Jun 2020 14:17:34 +0200 wenzelm clarified errors;
Thu, 11 Jun 2020 16:13:53 +0100 paulson fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
Thu, 11 Jun 2020 14:18:34 +0200 wenzelm tuned whitespace;
Thu, 11 Jun 2020 14:13:04 +0200 wenzelm proper rendering of complex codepoints, e.g. \<^url> code: 0x01F310;
Wed, 10 Jun 2020 19:59:12 +0200 wenzelm updated to jedit-5.6pre1 (repository version 25349);
Wed, 10 Jun 2020 15:55:41 +0200 blanchet simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
Tue, 09 Jun 2020 12:13:15 +0100 paulson New Ackermann development
Mon, 08 Jun 2020 22:49:06 +0200 wenzelm tuned document;
Mon, 08 Jun 2020 22:31:36 +0200 wenzelm proper latex macros, notably for src/HOL/Examples/Iff_Oracle.thy;
Mon, 08 Jun 2020 21:56:06 +0200 wenzelm NEWS;
Mon, 08 Jun 2020 21:55:14 +0200 wenzelm clarified sessions;
Mon, 08 Jun 2020 21:38:41 +0200 wenzelm clarified sessions: "Notable Examples in Isabelle/HOL";
Mon, 08 Jun 2020 15:09:57 +0200 wenzelm clarified sessions: "Notable Examples in Isabelle/Pure";
Sat, 06 Jun 2020 10:58:13 +0200 haftmann NEWS
Thu, 04 Jun 2020 19:38:52 +0000 haftmann more theorems
Thu, 04 Jun 2020 19:38:50 +0000 haftmann avoid overaggressive default simp rules
Thu, 04 Jun 2020 15:30:22 +0000 haftmann activate simproc for FOL
Thu, 04 Jun 2020 15:30:22 +0000 haftmann more rules for FOL also
Thu, 04 Jun 2020 15:30:22 +0000 haftmann more simp rules
Wed, 03 Jun 2020 11:44:21 +0200 nipkow should have been copied across from Set.thy as well for better printing
Sat, 30 May 2020 11:48:35 +0000 haftmann specific atomization inert to later rule set modifications
Sat, 30 May 2020 11:48:28 +0000 haftmann more precise scope of atomize
Sat, 30 May 2020 08:50:18 +0000 haftmann install simproc but deactivate by default
Wed, 27 May 2020 21:02:44 +0200 wenzelm adapted to d25093536482;
Wed, 27 May 2020 20:51:25 +0200 wenzelm clarified markup;
Wed, 27 May 2020 20:38:59 +0200 wenzelm clarified signature;
Wed, 27 May 2020 20:02:02 +0200 wenzelm tuned signature;
Wed, 27 May 2020 16:43:34 +0200 wenzelm tuned;
Wed, 27 May 2020 16:09:25 +0200 wenzelm more NEWS;
Wed, 27 May 2020 16:05:17 +0200 wenzelm more documentation on Isabelle/Scala;
Wed, 27 May 2020 16:04:53 +0200 wenzelm proper error positions;
Wed, 27 May 2020 15:51:10 +0200 wenzelm tuned;
Wed, 27 May 2020 14:33:03 +0200 wenzelm tuned whitespace;
Wed, 27 May 2020 14:32:51 +0200 wenzelm more antiquotations;
Wed, 27 May 2020 14:27:22 +0200 wenzelm check bash functions against Isabelle settings environment;
Wed, 27 May 2020 13:57:13 +0200 wenzelm misc tuning;
Wed, 27 May 2020 13:22:17 +0200 wenzelm breakable scala_name;
Tue, 26 May 2020 22:45:05 +0200 wenzelm tuned signature;
Tue, 26 May 2020 19:59:13 +0200 wenzelm discontinued pointless document antiquotation;
Tue, 26 May 2020 12:09:36 +0200 wenzelm proper check of example;
Tue, 26 May 2020 11:58:42 +0200 wenzelm clarified signature --- fit within limit of 22 arguments;
Tue, 26 May 2020 11:25:33 +0200 wenzelm tuned;
Tue, 26 May 2020 11:17:10 +0200 wenzelm tuned;
Mon, 25 May 2020 22:37:22 +0200 wenzelm more antiquotations;
Mon, 25 May 2020 22:37:14 +0200 wenzelm obsolete;
Mon, 25 May 2020 22:20:21 +0200 wenzelm check free-form Scala source;
Mon, 25 May 2020 20:52:55 +0200 wenzelm clarified static_check: avoid accidental evaluation;
Mon, 25 May 2020 20:46:50 +0200 wenzelm omit pointless memoing: Scala compiler is rather bulky anyway;
Mon, 25 May 2020 20:43:19 +0200 wenzelm clarified signature;
Mon, 25 May 2020 19:10:38 +0200 wenzelm antiquotations for Scala entities;
Sun, 24 May 2020 19:57:13 +0000 haftmann better closeup and more consistent terminology
Sun, 24 May 2020 21:11:23 +0200 wenzelm merged
Sun, 24 May 2020 21:01:51 +0200 wenzelm proper stack_limit;
Sun, 24 May 2020 20:59:34 +0200 wenzelm clarified signature;
Sun, 24 May 2020 20:35:24 +0200 wenzelm more accurate classpath for "isabelle scala";
Sun, 24 May 2020 19:45:42 +0200 wenzelm proper check of registered Scala functions;
Sun, 24 May 2020 14:47:28 +0200 wenzelm asynchronous build_session: notably for Scala.fulfill protocol commands during run;
Sun, 24 May 2020 14:15:44 +0200 wenzelm clarified build_session protocol;
Sun, 24 May 2020 13:39:45 +0200 wenzelm clarified signature;
Sun, 24 May 2020 12:43:04 +0200 wenzelm clarified name;
Sun, 24 May 2020 12:38:41 +0200 wenzelm more robust: explicit check for PIDE session;
Sun, 24 May 2020 10:36:42 +0200 wenzelm tuned signature;
Sun, 24 May 2020 10:28:04 +0200 wenzelm unused;
Sat, 23 May 2020 22:09:55 +0200 wenzelm tuned signature;
Sat, 23 May 2020 21:58:44 +0200 wenzelm check Scala source snippets from ML;
Sat, 23 May 2020 21:43:30 +0200 wenzelm more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
Sat, 23 May 2020 12:04:24 +0200 wenzelm init default context;
Sat, 23 May 2020 11:33:45 +0200 wenzelm tuned message;
Sat, 23 May 2020 11:27:35 +0200 wenzelm clarified signature;
(0) -30000 -10000 -3000 -1000 -192 +192 +1000 +3000 +10000 tip