| Mon, 04 Nov 2013 10:52:41 +0100 |
blanchet |
moved code around
|
file |
diff |
annotate
|
| Tue, 22 Oct 2013 14:17:12 +0200 |
traytel |
define a trivial nonemptiness witness if none is provided
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 17:47:25 +0200 |
blanchet |
don't print BNF constants
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 15:42:55 +0200 |
blanchet |
conceal even more ugly constructions
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 22:59:19 +0200 |
traytel |
keep the qualification of bindings when noting bnf theorems
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 11:23:49 +0200 |
traytel |
simplified derivation of in_rel
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 23:01:04 +0200 |
blanchet |
renamed BNF fact
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 22:56:39 +0200 |
blanchet |
renamed BNF axiom
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 22:39:46 +0200 |
blanchet |
renamed BNF fact
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 22:39:46 +0200 |
blanchet |
renamed BNF axiom
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 22:39:46 +0200 |
blanchet |
renamed BNF fact
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 18:44:03 +0200 |
blanchet |
renamed BNF axiom
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 17:20:17 +0200 |
blanchet |
qualify BNF constants properly
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 11:19:27 +0200 |
panny |
removed outdated comments
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 17:13:46 +0200 |
traytel |
configuration option to control timing output for (co)datatypes
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 13:48:25 +0200 |
traytel |
transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids non-trivial merges)
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 19:03:31 +0200 |
blanchet |
renamed function
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 18:56:33 +0200 |
blanchet |
eliminate quasi-duplicate function
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 15:35:47 +0200 |
blanchet |
moved useful library functions upstream
|
file |
diff |
annotate
|
| Sun, 11 Aug 2013 23:35:59 +0200 |
blanchet |
avoid DUP exception in local context (cf. 062aa11e98e1)
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 11:26:29 +0200 |
traytel |
tuned
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 22:36:31 +0200 |
traytel |
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 16:50:41 +0200 |
traytel |
more robust tactic
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 16:46:53 +0200 |
traytel |
transfer rule for {c,d}tor_{,un}fold
|
file |
diff |
annotate
|
| Wed, 24 Jul 2013 13:03:53 +0200 |
traytel |
proper transfer rule format for map_transfer
|
file |
diff |
annotate
|
| Tue, 23 Jul 2013 13:14:14 +0200 |
traytel |
transfer stored bnf theorems into the "current" theory when retrieving a bnf (avoids non-trivial merges)
|
file |
diff |
annotate
|
| Tue, 23 Jul 2013 13:10:27 +0200 |
traytel |
separate ML interface to note facts of a bnf
|
file |
diff |
annotate
|
| Mon, 22 Jul 2013 21:12:15 +0200 |
traytel |
transfer rule for map (not yet registered as a transfer rule)
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 13:03:21 +0200 |
traytel |
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
|
file |
diff |
annotate
|
| Sat, 11 May 2013 16:57:18 +0200 |
wenzelm |
prefer explicitly qualified exceptions, which is particular important for robust handlers;
|
file |
diff |
annotate
|