| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
more uniform approach towards satisfied applications
|
file |
diff |
annotate
|
| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
more uniform approach towards satisfied applications
|
file |
diff |
annotate
|
| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
Tuned semicolons.
|
file |
diff |
annotate
|
| Thu, 09 Feb 2023 13:50:09 +0100 |
stuebinm |
explicit range types in abstractions
|
file |
diff |
annotate
|
| Sun, 12 Feb 2023 06:45:59 +0000 |
haftmann |
somehow more clear terminology
|
file |
diff |
annotate
|
| Sun, 12 Feb 2023 06:45:58 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 02 Apr 2022 17:03:35 +0000 |
haftmann |
pass constructor arity as part of case certficiate
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 16:41:16 +0000 |
haftmann |
tuned, centralizing case distinction at one place at the cost of modest duplication
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 10:54:40 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 10:54:40 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 29 Mar 2022 06:02:17 +0000 |
haftmann |
tighter check to ensure that patterns remain left-linear, previous implementation was overcautious
|
file |
diff |
annotate
|
| Tue, 29 Mar 2022 06:02:16 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 29 Mar 2022 06:02:14 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 28 Mar 2022 12:54:13 +0000 |
haftmann |
separated treatment of undefined bodys
|
file |
diff |
annotate
|
| Mon, 28 Mar 2022 12:54:11 +0000 |
haftmann |
tuned arguments
|
file |
diff |
annotate
|
| Mon, 28 Mar 2022 12:54:09 +0000 |
haftmann |
modernized handling of variables
|
file |
diff |
annotate
|
| Sun, 27 Mar 2022 19:27:54 +0000 |
haftmann |
structurally tuned
|
file |
diff |
annotate
|
| Sun, 27 Mar 2022 19:27:53 +0000 |
haftmann |
tuned names
|
file |
diff |
annotate
|
| Sun, 27 Mar 2022 19:27:52 +0000 |
haftmann |
prefer build combinator
|
file |
diff |
annotate
|
| Sun, 27 Mar 2022 19:27:50 +0000 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:44 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:43 +0000 |
haftmann |
separated case reduction
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:42 +0000 |
haftmann |
separated selector function entirely
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:41 +0000 |
haftmann |
self-contained extraction auf clauses
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:40 +0000 |
haftmann |
extracted selector function, restoring code generation for let expressions
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:39 +0000 |
haftmann |
streamlined
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:38 +0000 |
haftmann |
streamlined
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:37 +0000 |
haftmann |
streamlined
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 16:34:35 +0000 |
haftmann |
disentangled
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 19:25:31 +0200 |
wenzelm |
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
|
file |
diff |
annotate
|
| Mon, 04 Oct 2021 19:12:24 +0200 |
wenzelm |
proper term operation Term.dest_abs;
|
file |
diff |
annotate
|
| Mon, 04 Oct 2021 18:19:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 02 Oct 2021 12:59:16 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2019 18:40:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2018 14:49:21 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 24 Jun 2017 09:17:33 +0200 |
haftmann |
treat "undefined" constants internally as special form of case combinators
|
file |
diff |
annotate
|
| Thu, 13 Apr 2017 10:10:12 +0200 |
haftmann |
for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
|
file |
diff |
annotate
|
| Thu, 26 Jan 2017 16:06:19 +0100 |
haftmann |
tuned structure and terminology
|
file |
diff |
annotate
|
| Tue, 14 Jun 2016 20:48:41 +0200 |
haftmann |
explicit resolution of ambiguous dictionaries
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:43:18 +0200 |
haftmann |
explicit check that abstract constructors cannot be part of official interface
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
optional timing for code generator conversions
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
corrected closure scope of static_conv_thingol;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified proof context vs. background theory
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified naming conventions and code for code evaluation sandwiches
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified names of variants
|
file |
diff |
annotate
|
| Mon, 09 May 2016 14:37:47 +0200 |
wenzelm |
clarified context, notably for internal use of Simplifier;
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 21:07:48 +0100 |
haftmann |
explicit record values for dictionary variables
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 21:07:47 +0100 |
haftmann |
provide explicit hint concering uniqueness of derivation
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 00:39:49 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 27 Apr 2015 16:46:52 +0200 |
wenzelm |
code equations as displayable content in code dependency graph
|
file |
diff |
annotate
|
| Mon, 27 Apr 2015 15:53:11 +0200 |
wenzelm |
filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 15:22:44 +0200 |
wenzelm |
discontinued pointless warnings: commands are only defined inside a theory context;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 11:22:36 +0200 |
wenzelm |
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 11:53:18 +0100 |
wenzelm |
clarified input source;
|
file |
diff |
annotate
|