| Thu, 23 Jan 2025 22:29:38 +0100 |
wenzelm |
tuned names: follow HOL Light;
|
file |
diff |
annotate
|
| Thu, 23 Jan 2025 22:20:40 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 23 Jan 2025 20:06:14 +0100 |
wenzelm |
proper treatment of variables with the same name, but different sorts/types: this routinely happens in HOL Light (see also 0e2f019477e2), as well as theory "HOL-Algebra.Algebraic_Closure_Type" (line 77);
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 23:28:34 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 23:17:21 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 23:15:03 +0100 |
wenzelm |
more direct emulation of HOL Light inferences: prefer Pure rules over HOL thms;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 19:49:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 19:26:39 +0100 |
wenzelm |
misc tuning: prefer specific variants of Thm.dest_comb;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 16:59:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 16:50:46 +0100 |
wenzelm |
more robust: explicit check for "Trueprop";
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 16:22:15 +0100 |
wenzelm |
clarified signature: more uniform cterm operations, without context;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 15:48:39 +0100 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 00:01:31 +0100 |
wenzelm |
tuned names, following HOL Light sources;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2025 23:00:17 +0100 |
wenzelm |
more comments;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2025 22:53:51 +0100 |
wenzelm |
cleanup generated bounds;
|
file |
diff |
annotate
|
| Sun, 19 Jan 2025 15:13:42 +0100 |
wenzelm |
support tracing (with proper guard);
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 13:20:47 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 13:10:09 +0100 |
wenzelm |
misc cleanup and minor performance tuning;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 12:53:23 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 12:45:33 +0100 |
wenzelm |
tuned: prefer existing operations;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 12:43:24 +0100 |
wenzelm |
tuned source structure;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 12:25:23 +0100 |
wenzelm |
tuned state operations;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 12:08:13 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 12:05:56 +0100 |
wenzelm |
misc tuning and clarification: prefer state operations, avoid redundant ctyp_of/cterm_of;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2025 11:09:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 20:30:01 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 19:56:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 17:01:43 +0100 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 16:49:01 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 16:22:49 +0100 |
wenzelm |
clarified exceptions and messages: use "error" only for user-errors, not system failures;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 16:13:48 +0100 |
wenzelm |
minor performance tuning: more elementary operations;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 16:03:35 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 15:39:40 +0100 |
wenzelm |
clarified inst_type: more direct Thm.instantiate_frees;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 14:47:25 +0100 |
wenzelm |
more direct Thm.free: avoid re-certification;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 14:31:48 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 13:44:45 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 13:04:34 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 13:00:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 12:50:46 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 12:46:50 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 12:41:01 +0100 |
wenzelm |
clarified signature: more standard Isabelle/ML;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 12:19:11 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 12:10:59 +0100 |
wenzelm |
more robust import_file path: proper master_directory;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 11:47:47 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 11:05:36 +0100 |
wenzelm |
clarified pattern via antiquotations;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 11:01:44 +0100 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 10:56:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 10:53:30 +0100 |
wenzelm |
clarified make_type: proper make_name;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 10:51:47 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 10:43:23 +0100 |
wenzelm |
clarified signature: more standard Isabelle/ML;
|
file |
diff |
annotate
|
| Thu, 16 Jan 2025 13:14:24 +0100 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
| Thu, 16 Jan 2025 12:45:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 16 Jan 2025 12:41:55 +0100 |
wenzelm |
tuned: prefer inlined thms;
|
file |
diff |
annotate
|
| Sun, 01 Dec 2024 14:01:47 +0100 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2023 21:03:16 +0100 |
wenzelm |
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 23:38:41 +0200 |
wenzelm |
clarified signature: File.read_lines is based on scalable Bytes.T;
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 10:55:23 +0200 |
wenzelm |
prefer scalable Bytes.T;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 11:27:23 +0200 |
wenzelm |
redundant: default is false;
|
file |
diff |
annotate
|
| Thu, 21 Feb 2019 09:15:07 +0000 |
haftmann |
streamlined specification interfaces
|
file |
diff |
annotate
|