src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
2013-05-02 blanchet 2013-05-02 renamings
2013-05-02 blanchet 2013-05-02 code tuning
2013-05-02 blanchet 2013-05-02 signature tuning
2013-05-02 blanchet 2013-05-02 removed dead code
2013-05-02 blanchet 2013-05-02 tuned signature
2013-05-02 blanchet 2013-05-02 store (co)induction rules in data structure
2013-05-02 blanchet 2013-05-02 tuning names
2013-05-02 blanchet 2013-05-02 export one more function
2013-05-02 blanchet 2013-05-02 rationalized data structure
2013-05-02 blanchet 2013-05-02 added and moved library functions (used in primrec code)
2013-05-02 blanchet 2013-05-02 tuned names -- co_ and un_ with underscore are to be understood as (co) and (un)
2013-05-02 blanchet 2013-05-02 tuning
2013-05-02 blanchet 2013-05-02 more code rationalization
2013-05-02 blanchet 2013-05-02 more code rationalization
2013-05-02 blanchet 2013-05-02 more code rationalization
2013-05-02 blanchet 2013-05-02 refactoring
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 tuning
2013-04-30 blanchet 2013-04-30 export more functions (useful for primrec_new)
2013-04-30 blanchet 2013-04-30 further enrich data structure
2013-04-30 blanchet 2013-04-30 more
2013-04-30 blanchet 2013-04-30 rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
2013-04-30 blanchet 2013-04-30 added fields to database
2013-04-30 blanchet 2013-04-30 tuned data structure
2013-04-30 blanchet 2013-04-30 renamed records
2013-04-30 blanchet 2013-04-30 added constructors to data structure
2013-04-30 blanchet 2013-04-30 added pre-BNFs to database
2013-04-30 blanchet 2013-04-30 lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
2013-04-30 blanchet 2013-04-30 Added maps, sets, rels to "simps" thm collection
2013-04-30 blanchet 2013-04-30 comment tuning
2013-04-30 blanchet 2013-04-30 tuning
2013-04-30 blanchet 2013-04-30 tuning
2013-04-30 blanchet 2013-04-30 tuning
2013-04-30 blanchet 2013-04-30 signature tuning
2013-04-30 blanchet 2013-04-30 whitespace tuning
2013-04-30 blanchet 2013-04-30 tuned signature
2013-04-29 blanchet 2013-04-29 register all (co)datatypes in local data
2013-04-29 blanchet 2013-04-29 create data structure for storing (co)datatype information
2013-04-29 blanchet 2013-04-29 use record instead of big tuple
2013-04-29 blanchet 2013-04-29 use base names, not full names
2013-04-29 blanchet 2013-04-29 tune signatures
2013-04-29 blanchet 2013-04-29 tuning
2013-04-29 blanchet 2013-04-29 tuning
2013-04-29 blanchet 2013-04-29 tuned function signatures
2013-04-29 blanchet 2013-04-29 factored out derivation of coinduction, unfold, corec
2013-04-29 blanchet 2013-04-29 factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
2013-04-29 blanchet 2013-04-29 use record instead of huge tuple
2013-04-29 blanchet 2013-04-29 renamed BNF "(co)data" commands to names that are closer to their final names
2013-04-27 blanchet 2013-04-27 tuned ML and thy file names
2013-04-26 blanchet 2013-04-26 for compatibility, generate recursor arguments in the same order as old package
2013-04-26 blanchet 2013-04-26 tuning in preparation for actual changes
2013-04-26 blanchet 2013-04-26 started working on compatibility with old package's recursor
2013-04-26 blanchet 2013-04-26 more intuitive syntax for equality-style discriminators of nullary constructors
2013-04-26 blanchet 2013-04-26 put an underscore in prefix
2013-04-26 blanchet 2013-04-26 changed discriminator default: avoid mixing ctor and dtor views
2013-04-25 blanchet 2013-04-25 renamed "wrap_data" to "wrap_free_constructors"
2013-04-25 blanchet 2013-04-25 register coinductive type's coinduct rule
2013-04-25 blanchet 2013-04-25 generate proper attributes for coinduction rules
2013-04-25 blanchet 2013-04-25 simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
2013-04-24 blanchet 2013-04-24 proper error generated for wrong mixfix