| 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
|
| Tue, 20 Aug 2013 17:39:07 +0200 |
traytel |
simpler (forward) derivation of strong (up-to equality) coinduction properties
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 16:10:58 +0200 |
traytel |
don't derive unused low-level theorem
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 15:30:25 +0200 |
traytel |
tuned
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 14:48:19 +0200 |
traytel |
tuned tactic;
|
file |
diff |
annotate
|
| Sun, 28 Jul 2013 12:59:59 +0200 |
traytel |
more converse(p) theorems; tuned proofs;
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 16:46:53 +0200 |
traytel |
transfer rule for {c,d}tor_{,un}fold
|
file |
diff |
annotate
|
| Mon, 15 Jul 2013 14:23:51 +0200 |
traytel |
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
|
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
|
| Thu, 11 Jul 2013 11:16:23 +0200 |
traytel |
some new lemmas towards getting rid of in_bd BNF property; tuned
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 10:24:00 +0200 |
traytel |
Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 20:41:41 +0200 |
traytel |
use long goal format in rel_induct theorem
|
file |
diff |
annotate
|
| Thu, 09 May 2013 20:44:37 +0200 |
traytel |
relator coinduction for codatatypes
|
file |
diff |
annotate
|
| Tue, 07 May 2013 14:22:54 +0200 |
traytel |
got rid of the set based relator---use (binary) predicate based relator instead
|
file |
diff |
annotate
|
| Wed, 01 May 2013 19:33:49 +0200 |
blanchet |
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
|
file |
diff |
annotate
|
| Sat, 27 Apr 2013 20:50:20 +0200 |
wenzelm |
uniform Proof.context for hyp_subst_tac;
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 19:18:20 +0200 |
traytel |
removed unnecessary assumptions in some theorems about cardinal exponentiation
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 17:47:22 +0200 |
blanchet |
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 14:15:01 +0200 |
blanchet |
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:43:09 +0200 |
traytel |
(co)rec is (just as the (un)fold) the unique morphism;
|
file |
diff |
annotate
|
| Mon, 18 Mar 2013 11:25:24 +0100 |
traytel |
eliminate duplicated constant (diag vs. Id_on)
|
file |
diff |
annotate
|
| Mon, 28 Jan 2013 23:56:13 +0100 |
traytel |
made SML/NJ happy
|
file |
diff |
annotate
|
| Tue, 13 Nov 2012 12:06:43 +0100 |
traytel |
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
|
file |
diff |
annotate
|
| Tue, 02 Oct 2012 09:20:28 +0200 |
traytel |
made tactic more robust (less usage of stac)
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
generate high-level "maps", "sets", and "rels" properties
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
renamed coinduction principles to have "dtor" in the name
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
renamed "map_simps" to "{c,d}tor_maps"
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 18:25:17 +0200 |
blanchet |
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 16:45:06 +0200 |
blanchet |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
|
file |
diff |
annotate
| base
|