src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-11-04 blanchet 2013-11-04 strengthened tactic
2013-10-24 blanchet 2013-10-24 got rid of annoying duplicate rewrite rule warnings
2013-09-18 blanchet 2013-09-18 avoid duplicate simp rule warnings
2013-09-12 blanchet 2013-09-12 made tactic handle gracefully the case: codatatype ('a, 's) scheduler2 = Combine2 "'s => 'a" "'s => ('a, 's) scheduler2"
2013-08-30 blanchet 2013-08-30 more canonical naming
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-12 blanchet 2013-08-12 define case constant from other 'free constructor' axioms
2013-08-12 blanchet 2013-08-12 tuning
2013-07-15 traytel 2013-07-15 eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
2013-06-07 blanchet 2013-06-07 code simplifications (cf. 78a3d5006cf1)
2013-06-07 blanchet 2013-06-07 changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 fixed failure in coinduction rule tactic
2013-05-30 wenzelm 2013-05-30 stay within regular tactic language -- avoid operating on whole proof state;
2013-05-29 blanchet 2013-05-29 generalized recursors, effectively reverting inductive half of c7a034d01936
2013-05-28 blanchet 2013-05-28 clean up list of theorems
2013-05-28 blanchet 2013-05-28 removed needless comment (yes, sum_case_if is needed)
2013-05-07 traytel 2013-05-07 got rid of the set based relator---use (binary) predicate based relator instead
2013-05-01 blanchet 2013-05-01 renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
2013-04-30 blanchet 2013-04-30 rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
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-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-10-02 blanchet 2012-10-02 continued changing type of corec type
2012-10-02 blanchet 2012-10-02 made (co)rec tactic more robust when the simplifier succeeds early
2012-10-01 blanchet 2012-10-01 fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
2012-10-01 blanchet 2012-10-01 tweaked corecursor/coiterator tactic
2012-10-01 blanchet 2012-10-01 changed the type of the recursor for nested recursion
2012-09-30 blanchet 2012-09-30 tuning
2012-09-30 traytel 2012-09-30 tuned tactic
2012-09-28 blanchet 2012-09-28 simplified simpset
2012-09-28 blanchet 2012-09-28 fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
2012-09-28 traytel 2012-09-28 tuned tactic
2012-09-28 traytel 2012-09-28 tuned tactic
2012-09-28 blanchet 2012-09-28 renamed ML file in preparation for next step