| Wed, 26 Oct 2016 22:40:28 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 13:35:29 +0200 |
blanchet |
prove 'set' property backward
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:16:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 10:09:33 +0200 |
blanchet |
tuned ML signature
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 20:57:07 +0200 |
blanchet |
exported ML functions
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 22:47:48 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2016 16:49:44 +0200 |
wenzelm |
eliminated pointless alias (no warning for duplicates);
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Mon, 11 Jan 2016 13:15:14 +0100 |
blanchet |
exported ML function
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 23:41:24 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 13:33:42 +0200 |
wenzelm |
explicit indication of overloaded typedefs;
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 12:21:19 +0200 |
traytel |
more useful properties of the relators
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 21:50:39 +0200 |
wenzelm |
more general Typedef.bindings;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 16:41:43 +0200 |
traytel |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 17:34:52 +0200 |
wenzelm |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:21:07 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 22:34:59 +0200 |
wenzelm |
support for strictly private name space entries;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 20:59:14 +0200 |
blanchet |
export more low-level theorems in data structure (partly for 'corec')
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 11:18:58 +0100 |
desharna |
generate 'disc_eq_case' for Ctr_Sugars
|
file |
diff |
annotate
|
| Thu, 11 Dec 2014 14:14:18 +0100 |
traytel |
conceal typedef more violently
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 20:41:53 +0100 |
wenzelm |
proper proof context for typedef;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 11:08:26 +0100 |
wenzelm |
proper syntax categery "name" -- as usual and as documented;
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 16:17:36 +0200 |
desharna |
generate 'sel_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 21:41:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:49 +0200 |
desharna |
add 'disc_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:39 +0200 |
desharna |
add 'case_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:24 +0200 |
desharna |
add 'ctr_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|