Wed, 18 Sep 2019 21:35:21 +0200 |
wenzelm |
proper export of result_text for 'have';
|
file |
diff |
annotate
|
Wed, 18 Sep 2019 20:53:53 +0200 |
wenzelm |
support soft types for 'assume';
|
file |
diff |
annotate
|
Wed, 18 Sep 2019 20:10:15 +0200 |
wenzelm |
more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);
|
file |
diff |
annotate
|
Tue, 17 Sep 2019 17:06:05 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 17 Sep 2019 16:26:57 +0200 |
wenzelm |
clarified signature -- removed unused option (see acb0807ddb56);
|
file |
diff |
annotate
|
Tue, 13 Aug 2019 10:27:21 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
Tue, 23 Jul 2019 12:07:50 +0200 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
Tue, 16 Jul 2019 15:39:32 +0200 |
wenzelm |
support for a soft-type system within the Isabelle logical framework;
|
file |
diff |
annotate
|
Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Sun, 23 Sep 2018 21:49:31 +0200 |
wenzelm |
discontinued old-style goal cases;
|
file |
diff |
annotate
|
Sun, 02 Sep 2018 19:48:15 +0200 |
wenzelm |
clarified reset_notepad;
|
file |
diff |
annotate
|
Sun, 02 Sep 2018 13:53:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Fri, 31 Aug 2018 22:25:58 +0200 |
wenzelm |
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
|
file |
diff |
annotate
|
Wed, 09 May 2018 20:45:57 +0200 |
wenzelm |
clarified future scheduling parameters, with support for parallel_limit;
|
file |
diff |
annotate
|