src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
2013-09-09 blanchet 2013-09-09 enriched data structure with necessary theorems
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-29 blanchet 2013-08-29 renamed BNF axiom
2013-08-29 blanchet 2013-08-29 merge
2013-08-29 blanchet 2013-08-29 handle type class annotations on (co)datatype parameters gracefully
2013-08-29 traytel 2013-08-29 store nesting_bnfs in fp_sugar (required in "nested to mutual" reduction)
2013-08-29 blanchet 2013-08-29 cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
2013-08-29 blanchet 2013-08-29 qualify generated constants uniformly
2013-08-29 blanchet 2013-08-29 rationalize message generation + added a warning
2013-08-29 traytel 2013-08-29 build relator term for compound type (generalized build_map)
2013-08-29 blanchet 2013-08-29 documentation ideas
2013-08-29 blanchet 2013-08-29 more
2013-08-28 blanchet 2013-08-28 better error message
2013-08-28 blanchet 2013-08-28 tuning
2013-08-26 blanchet 2013-08-26 simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
2013-08-26 traytel 2013-08-26 moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
2013-08-22 traytel 2013-08-22 configuration option to control timing output for (co)datatypes
2013-08-21 traytel 2013-08-21 transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids non-trivial merges)
2013-08-20 traytel 2013-08-20 moved derivation of strong coinduction to sugar
2013-08-16 blanchet 2013-08-16 tuning
2013-08-16 blanchet 2013-08-16 moved function to where it seems to belong
2013-08-16 blanchet 2013-08-16 moved library function where it belongs, and used Dmitriy's inside-out implementation
2013-08-16 blanchet 2013-08-16 added useful library function
2013-08-16 traytel 2013-08-16 tuned
2013-08-16 blanchet 2013-08-16 moved useful library functions upstream
2013-08-14 blanchet 2013-08-14 added fixme
2013-08-12 blanchet 2013-08-12 clarified option name (since case/fold/rec are also destructors)
2013-08-12 blanchet 2013-08-12 define case constant from other 'free constructor' axioms
2013-08-12 blanchet 2013-08-12 qualify map and rel names
2013-08-11 blanchet 2013-08-11 made (hopefully temporary) hack more robust
2013-08-11 blanchet 2013-08-11 added warning
2013-08-11 blanchet 2013-08-11 gracefully handle one more error condition
2013-08-11 blanchet 2013-08-11 gracefully fail to define polymorphic (co)datatypes in local context
2013-08-09 traytel 2013-08-09 tuned
2013-08-07 blanchet 2013-08-07 tuning
2013-08-07 blanchet 2013-08-07 enrich exported ML function's signature
2013-08-06 blanchet 2013-08-06 tuning
2013-08-06 blanchet 2013-08-06 tuning
2013-08-06 blanchet 2013-08-06 tuning
2013-08-06 blanchet 2013-08-06 tuning
2013-08-06 blanchet 2013-08-06 export ML function (for primcorec)
2013-08-01 blanchet 2013-08-01 tuning
2013-07-30 blanchet 2013-07-30 avoid DUP error in local context
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-15 traytel 2013-07-15 eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
2013-06-11 blanchet 2013-06-11 tuning
2013-06-11 blanchet 2013-06-11 tuning
2013-06-10 blanchet 2013-06-10 use right context when exporting variables (cf. AFP Coinductive_List failures)
2013-06-10 blanchet 2013-06-10 keep track of nested BNFs
2013-06-10 blanchet 2013-06-10 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 code simplifications (cf. 78a3d5006cf1)
2013-06-07 blanchet 2013-06-07 killed dead code
2013-06-07 blanchet 2013-06-07 changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
2013-06-07 blanchet 2013-06-07 killed dead code
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning