| 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
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 22:38:44 +0100 |
wenzelm |
take qualification of type name more seriously: derived consts and facts are qualified uniformly;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2016 17:01:21 +0100 |
wenzelm |
no tracing SPAM, and thus more visible warnings;
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 13:33:42 +0200 |
wenzelm |
explicit indication of overloaded typedefs;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 21:50:39 +0200 |
wenzelm |
more general Typedef.bindings;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 22:07:09 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 20:49:28 +0100 |
wenzelm |
proper context for typedef;
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
added flag to 'typedef' to allow concealed definitions
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 16:19:24 +0100 |
wenzelm |
proper Sign.full_name to get internal name (like Sign.add_consts);
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 20:42:16 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 10:45:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 21:22:35 +0200 |
wenzelm |
discontinued typedef with alternative name;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 15:08:29 +0200 |
wenzelm |
discontinued typedef with implicit set_def;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 12:47:49 +0200 |
wenzelm |
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
|
file |
diff |
annotate
|
| Thu, 05 Apr 2012 08:43:31 +0200 |
krauss |
added timestamps to logging of named thms
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 20:09:56 +0200 |
Cezary Kaliszyk |
HOL/Import typed matches against Isabelle typedef result
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 14:50:47 +0200 |
Cezary Kaliszyk |
Modernized HOL-Import for HOL Light
|
file |
diff |
annotate
|