src/HOL/BNF/Tools/bnf_def_tactics.ML
2014-01-12 wenzelm 2014-01-12 tuned signature; clarified context;
2013-12-18 traytel 2013-12-18 express weak pullback property of bnfs only in terms of the relator
2013-12-17 traytel 2013-12-17 tuned
2013-10-22 traytel 2013-10-22 define a trivial nonemptiness witness if none is provided
2013-09-12 traytel 2013-09-12 handle corner case in tactic
2013-09-12 traytel 2013-09-12 simplified derivation of in_rel
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-29 blanchet 2013-08-29 renamed BNF axiom
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-29 blanchet 2013-08-29 renamed BNF axiom
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-29 blanchet 2013-08-29 renamed BNF axiom
2013-08-12 traytel 2013-08-12 eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)
2013-08-02 traytel 2013-08-02 more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
2013-07-31 traytel 2013-07-31 more robust tactic
2013-07-28 traytel 2013-07-28 more converse(p) theorems; tuned proofs;
2013-07-25 traytel 2013-07-25 transfer rule for {c,d}tor_{,un}fold
2013-07-24 traytel 2013-07-24 proper transfer rule format for map_transfer
2013-07-22 traytel 2013-07-22 transfer rule for map (not yet registered as a transfer rule)
2013-07-15 traytel 2013-07-15 eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
2013-07-13 traytel 2013-07-13 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
2013-05-08 traytel 2013-05-08 stronger monotonicity property for relators
2013-05-08 traytel 2013-05-08 make tactic actually work for op = as relator
2013-05-07 traytel 2013-05-07 tuned
2013-05-07 traytel 2013-05-07 got rid of the set based relator---use (binary) predicate based relator instead
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-24 blanchet 2013-04-24 renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
2013-04-24 blanchet 2013-04-24 derive "map_cong"
2013-04-24 blanchet 2013-04-24 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
2012-09-27 traytel 2012-09-27 tuned tactic; got rid of substs_tac alias
2012-09-27 traytel 2012-09-27 tuned tactic
2012-09-26 blanchet 2012-09-26 parameterized "subst_tac"
2012-09-21 blanchet 2012-09-21 renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"