| 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
|
| Mon, 06 Oct 2014 13:34:12 +0200 |
desharna |
add 'set_cases' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:04 +0200 |
desharna |
add 'set_intros' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:45 +0200 |
desharna |
add 'set_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:24 +0200 |
desharna |
add 'rel_cases' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:15 +0200 |
desharna |
add 'rel_intros' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:04 +0200 |
desharna |
add 'rel_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:32:53 +0200 |
desharna |
add 'map_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 23:09:04 +0200 |
blanchet |
removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
added flag to 'typedef' to allow concealed definitions
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
file |
diff |
annotate
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
refactor some tactics
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 21:15:57 +0200 |
blanchet |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 19:51:00 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:33:06 +0200 |
blanchet |
changed '-:' to 'dead' in BNF
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 00:54:30 +0200 |
blanchet |
cleaner 'rel_inject' theorems
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
manual merge + added 'rel_distincts' field to record for symmetry
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
generate 'rec_o_map' and 'size_o_map' in size extension
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
added 'inj_map' as auxiliary BNF theorem
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:16 +0200 |
kuncar |
export theorems
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
got rid of automatically generated fold constant and theorems (to reduce overhead)
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 18:14:26 +0100 |
traytel |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 13:04:57 +0100 |
blanchet |
correct most general type for mutual recursion when several identical types are involved
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 08:33:59 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:08:59 +0100 |
blanchet |
prepare two-stage 'primrec' setup
|
file |
diff |
annotate
|