| Mon, 01 Sep 2014 16:34:40 +0200 |
blanchet |
renamed BNF theories
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 10:43:03 +0200 |
traytel |
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorems in 'BNF_Comp'
|
file |
diff |
annotate
|
| Thu, 17 Jul 2014 10:28:32 +0200 |
desharna |
add mk_Trueprop_mem utility function
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:24:49 +0100 |
traytel |
copy-paste typo
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:23:16 +0100 |
traytel |
unfold intermediate definitions after sealing the bnf
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 22:27:04 +0100 |
traytel |
more careful unfolding of internal constants
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 21:40:41 +0100 |
traytel |
made typedef for the type of the bound optional (size-based)
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 23:09:10 +0100 |
traytel |
removed junk
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:25:55 +0100 |
traytel |
tuned
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:14:54 +0100 |
traytel |
move special BNFs used for composition only to BNF_Comp;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:17:26 +0100 |
traytel |
more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 22:30:12 +0100 |
blanchet |
no 'sorry' so that the schematic variable gets instantiated
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 18:57:17 +0100 |
blanchet |
simplify sets in BNF composition
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 18:57:17 +0100 |
blanchet |
more caching in composition pipeline
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 13:38:02 +0100 |
traytel |
propagate the exception that is expected later on
|
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
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
use same identity function for abs and rep (doesn't seem to confuse any proofs)
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
make 'typedef' optional, depending on size of original type
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
use aconv to compare terms (for cleanliness)
|
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
|
| Mon, 24 Feb 2014 10:16:10 +0100 |
traytel |
clarified interaction with dead variables in the composition of BNFs
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 00:04:48 +0100 |
blanchet |
added BNF cache (within one definition)
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 22:51:11 +0100 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 22:51:11 +0100 |
blanchet |
optimized 'bnf_of_typ' further w.r.t. dead variables
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 22:51:11 +0100 |
blanchet |
optimization of 'bnf_of_typ' if all variables are dead
|
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
|
| 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 |
adjusted comments
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
avoid nested 'Tools' directories
|
file |
diff |
annotate
| base
|