| 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
|