src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
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
2013-04-24 blanchet 2013-04-24 honor user-specified name for relator + generalize syntax
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 honor user-specified name for map function
2013-04-24 blanchet 2013-04-24 honor user-specified set function names
2013-04-24 blanchet 2013-04-24 parse set function name
2013-04-23 blanchet 2013-04-23 avoid accidental specialization of the types in the "map" property of codatatypes
2013-04-23 blanchet 2013-04-23 simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-08 blanchet 2013-03-08 proper type inference for default values
2012-11-22 traytel 2012-11-22 made SML/NJ happier
2012-10-03 blanchet 2012-10-03 thread the right local theory through + reenable parallel proofs for previously problematic theories
2012-10-02 blanchet 2012-10-02 continued changing type of corec type
2012-10-02 blanchet 2012-10-02 removed dead params and dead code
2012-10-02 blanchet 2012-10-02 changed type of corecursor for the nested recursion case
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-28 blanchet 2012-09-28 renamed ML file in preparation for next step