src/HOL/BNF/Tools/bnf_gfp_tactics.ML
Wed, 18 Dec 2013 11:03:40 +0100 traytel express weak pullback property of bnfs only in terms of the relator
Tue, 17 Dec 2013 15:44:10 +0100 traytel tighter bnf bounds for (co)datatypes
Thu, 29 Aug 2013 22:56:39 +0200 blanchet renamed BNF axiom
Thu, 29 Aug 2013 22:39:46 +0200 blanchet renamed BNF fact
Thu, 29 Aug 2013 22:39:46 +0200 blanchet renamed BNF axiom
Thu, 29 Aug 2013 22:39:46 +0200 blanchet renamed BNF fact
Thu, 29 Aug 2013 18:44:03 +0200 blanchet renamed BNF axiom
Tue, 20 Aug 2013 17:39:07 +0200 traytel simpler (forward) derivation of strong (up-to equality) coinduction properties
Tue, 20 Aug 2013 16:10:58 +0200 traytel don't derive unused low-level theorem
Thu, 08 Aug 2013 15:30:25 +0200 traytel tuned
Thu, 08 Aug 2013 14:48:19 +0200 traytel tuned tactic;
Sun, 28 Jul 2013 12:59:59 +0200 traytel more converse(p) theorems; tuned proofs;
Thu, 25 Jul 2013 16:46:53 +0200 traytel transfer rule for {c,d}tor_{,un}fold
Mon, 15 Jul 2013 14:23:51 +0200 traytel eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
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)
Thu, 11 Jul 2013 11:16:23 +0200 traytel some new lemmas towards getting rid of in_bd BNF property; tuned
Sun, 07 Jul 2013 10:24:00 +0200 traytel Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
Wed, 03 Jul 2013 20:41:41 +0200 traytel use long goal format in rel_induct theorem
Thu, 09 May 2013 20:44:37 +0200 traytel relator coinduction for codatatypes
Tue, 07 May 2013 14:22:54 +0200 traytel got rid of the set based relator---use (binary) predicate based relator instead
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
Sat, 27 Apr 2013 20:50:20 +0200 wenzelm uniform Proof.context for hyp_subst_tac;
Thu, 25 Apr 2013 19:18:20 +0200 traytel removed unnecessary assumptions in some theorems about cardinal exponentiation
Wed, 24 Apr 2013 17:47:22 +0200 blanchet renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
Wed, 24 Apr 2013 14:15:01 +0200 blanchet renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
Tue, 23 Apr 2013 11:43:09 +0200 traytel (co)rec is (just as the (un)fold) the unique morphism;
Mon, 18 Mar 2013 11:25:24 +0100 traytel eliminate duplicated constant (diag vs. Id_on)
Mon, 28 Jan 2013 23:56:13 +0100 traytel made SML/NJ happy
Tue, 13 Nov 2012 12:06:43 +0100 traytel import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
Tue, 02 Oct 2012 09:20:28 +0200 traytel made tactic more robust (less usage of stac)
Wed, 26 Sep 2012 10:00:59 +0200 blanchet generate high-level "maps", "sets", and "rels" properties
Wed, 26 Sep 2012 10:00:59 +0200 blanchet renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
Sun, 23 Sep 2012 14:52:53 +0200 blanchet renamed coinduction principles to have "dtor" in the name
Sun, 23 Sep 2012 14:52:53 +0200 blanchet renamed "set_incl" etc. to have "ctor" or "dtor" in the name
Sun, 23 Sep 2012 14:52:53 +0200 blanchet renamed low-level "map_unique" to have "ctor" or "dtor" in the name
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
Sun, 23 Sep 2012 14:52:53 +0200 blanchet renamed "map_simps" to "{c,d}tor_maps"
Fri, 21 Sep 2012 18:25:17 +0200 blanchet renamed "rel_simp" to "dtor_rel" and similarly for "srel"
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"
less more (0) tip