| Thu, 17 Jul 2014 10:28:32 +0200 |
desharna |
add mk_Trueprop_mem utility function
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:58:38 +0200 |
blanchet |
don't conceal (co)datatypes
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 00:54:30 +0200 |
blanchet |
more reliable 'name_of_bnf'
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 15:14:38 +0200 |
traytel |
more accurate type arguments for intermeadiate typedefs
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 10:51:29 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 10:51:29 +0200 |
blanchet |
added BNF interpretation hook
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:14:33 +0100 |
traytel |
prove theorems with fixed variables (export afterwards)
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 17:35:39 +0100 |
traytel |
tuned internal construction
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 16:28:25 +0100 |
traytel |
tuned tactics
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 11:15:04 +0100 |
traytel |
simplified internal codatatype construction
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 14:46:22 +0100 |
traytel |
tuned tactic
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:23:16 +0100 |
traytel |
unfold intermediate definitions after sealing the bnf
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 18:57:17 +0100 |
blanchet |
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 12:32:33 +0100 |
traytel |
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 09:29:56 +0100 |
blanchet |
removed debugging leftover
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
optimize cardinal bounds involving natLeq (omega)
|
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
|
| Wed, 26 Feb 2014 23:09:29 +0100 |
traytel |
intermediate typedef for the type of the bound (local to lfp)
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:10:38 +0100 |
traytel |
made tactics more robust
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 12:33:49 +0100 |
traytel |
only one internal coinduction rule
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 11:40:03 +0100 |
traytel |
made tactics more robust
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 12:04:21 +0100 |
traytel |
another simplification of internal codatatype construction
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 09:50:50 +0100 |
traytel |
simplifications of internal codatatype construction
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 14:51:26 +0100 |
traytel |
syntactic simplifications of internal (co)datatype constructions
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 18:18:27 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
tuning: moved code where it belongs
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 13:45:29 +0100 |
traytel |
register bnfs for (co)datatypes under their proper name (lost in af71b753c459)
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
adapted theories to '{case,rec}_{list,option}' names
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 12:16:59 +0100 |
traytel |
use Local_Theory.define instead of Specification.definition for internal constants
|
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 |
tuned names
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
made BNF compile after move to HOL
|
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
|