Sat, 13 Apr 2019 22:06:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 13 Apr 2019 16:26:19 +0200 |
wenzelm |
tuned signature -- more ctyp operations;
|
file |
diff |
annotate
|
Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
Thu, 14 Apr 2016 15:33:51 +0200 |
wenzelm |
misc tuning and standardization;
|
file |
diff |
annotate
|
Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file |
diff |
annotate
|
Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit 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
|
Fri, 10 Apr 2015 18:23:01 +0200 |
blanchet |
renamed ML funs
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 06 Mar 2015 23:53:52 +0100 |
wenzelm |
clarified context;
|
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
|
Fri, 06 Mar 2015 00:00:57 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
Fri, 19 Dec 2014 20:10:59 +0100 |
wenzelm |
just one data slot per program unit;
|
file |
diff |
annotate
|
Fri, 19 Dec 2014 12:56:06 +0100 |
wenzelm |
proper exception for internal program failure, not user-error;
|
file |
diff |
annotate
|
Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
Mon, 08 Sep 2014 15:54:33 +0200 |
blanchet |
export right sorts
|
file |
diff |
annotate
|
Mon, 08 Sep 2014 14:03:57 +0200 |
blanchet |
use compatibility layer
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|