Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
Mon, 05 Jan 2015 10:09:42 +0100 |
blanchet |
added plugins syntax to prim(co)rec
|
file |
diff |
annotate
|
Thu, 11 Dec 2014 14:14:39 +0100 |
traytel |
note more facts (always)
|
file |
diff |
annotate
|
Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
Mon, 13 Oct 2014 19:34:10 +0200 |
wenzelm |
clarified load order;
|
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
|
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
|
Wed, 24 Sep 2014 16:35:42 +0200 |
blanchet |
improved 'bnf' parser
|
file |
diff |
annotate
|
Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
file |
diff |
annotate
|
Mon, 15 Sep 2014 16:14:14 +0200 |
blanchet |
set 'mono' attribute on 'rel_mono'
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
introduced mechanism to filter interpretations
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:00 +0200 |
blanchet |
centralized and cleaned up naming handling
|
file |
diff |
annotate
|
Wed, 03 Sep 2014 22:49:05 +0200 |
blanchet |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
file |
diff |
annotate
|
Wed, 03 Sep 2014 22:47:35 +0200 |
blanchet |
tuned BNF database handling
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
added theory-based getters for convenience
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 13:53:34 +0200 |
desharna |
generate 'set_transfer' for BNFs
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 13:23:39 +0200 |
desharna |
generate 'rel_transfer' for BNFs
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 13:23:00 +0200 |
desharna |
note 'map_transfer' more often
|
file |
diff |
annotate
|
Fri, 29 Aug 2014 14:21:24 +0200 |
desharna |
generate 'case_transfer' for (co)datatypes
|
file |
diff |
annotate
|
Mon, 18 Aug 2014 15:03:22 +0200 |
desharna |
generate 'map_cong_simp' for BNFs
|
file |
diff |
annotate
|
Mon, 18 Aug 2014 14:09:09 +0200 |
desharna |
generate 'inj_map_strong' for BNFs
|
file |
diff |
annotate
|
Mon, 18 Aug 2014 13:49:47 +0200 |
desharna |
note 'inj_map' more often
|
file |
diff |
annotate
|
Mon, 18 Aug 2014 13:46:26 +0200 |
desharna |
generate property 'rel_mono_strong' for BNFs
|
file |
diff |
annotate
|
Mon, 18 Aug 2014 13:46:22 +0200 |
desharna |
renamed 'rel_mono_strong' to 'rel_mono_strong0'
|
file |
diff |
annotate
|
Thu, 14 Aug 2014 13:20:54 +0200 |
desharna |
generate 'rel_map' theorem for BNFs
|
file |
diff |
annotate
|
Fri, 25 Jul 2014 11:26:10 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorems in 'BNF_Comp'
|
file |
diff |
annotate
|
Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, also in 'BNF_Def'
|
file |
diff |
annotate
|
Thu, 17 Jul 2014 10:28:32 +0200 |
desharna |
add mk_Trueprop_mem utility function
|
file |
diff |
annotate
|
Wed, 09 Jul 2014 11:35:52 +0200 |
blanchet |
got rid of a pointer equality
|
file |
diff |
annotate
|
Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
tune the implementation of 'rel_coinduct'
|
file |
diff |
annotate
|
Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
generate 'rel_coinduct0' theorem for codatatypes
|
file |
diff |
annotate
|
Thu, 08 May 2014 12:54:02 +0200 |
desharna |
note map_id0 more often
|
file |
diff |
annotate
|
Thu, 08 May 2014 11:52:44 +0200 |
desharna |
generate 'map_ident' theorem for BNFs
|
file |
diff |
annotate
|
Mon, 28 Apr 2014 00:54:30 +0200 |
blanchet |
more reliable 'name_of_bnf'
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 11:29:39 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
localize new size function generation code
|
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:17 +0200 |
kuncar |
revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
|
file |
diff |
annotate
|
Thu, 10 Apr 2014 17:48:16 +0200 |
kuncar |
don't forget to init Interpretation and transfer theorems in the interpretation hook
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 10:51:24 +0200 |
blanchet |
added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
|
file |
diff |
annotate
|
Tue, 01 Apr 2014 10:51:29 +0200 |
blanchet |
added BNF interpretation hook
|
file |
diff |
annotate
|
Mon, 10 Mar 2014 13:23:16 +0100 |
traytel |
unfold intermediate definitions after sealing the bnf
|
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 |
make 'typedef' optional, depending on size of original type
|
file |
diff |
annotate
|
Fri, 14 Feb 2014 15:03:24 +0100 |
blanchet |
allow different functions to recurse on the same type, like in the old package
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 17:36:00 +0100 |
blanchet |
iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
more liberal merging of BNFs and constructor sugar
|
file |
diff |
annotate
|
Fri, 07 Feb 2014 10:44:04 +0100 |
blanchet |
reverted a87e49f4336d -- overwriting of data entries yields to merge problems later
|
file |
diff |
annotate
|
Thu, 06 Feb 2014 17:05:47 +0100 |
blanchet |
allow multiple registration of the same type, the last wins
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 10:02:36 +0100 |
traytel |
less hermetic tactics
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
adjusted comments
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
avoid nested 'Tools' directories
|
file |
diff |
annotate
| base
|