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-02 nipkow 2013-05-02 tuned
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-05-01 nipkow 2013-05-01 tuned
2013-05-01 nipkow 2013-05-01 tuned
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 renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
2013-04-30 blanchet 2013-04-30 Added maps, sets, rels to "simps" thm collection
2013-04-30 nipkow 2013-04-30 tuned
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-30 nipkow 2013-04-30 canonical names of classes
2013-04-29 blanchet 2013-04-29 merged
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 wenzelm 2013-04-29 avoid empty isabelletags.sty for the sake of arXiv;
2013-04-29 wenzelm 2013-04-29 merged
2013-04-29 wenzelm 2013-04-29 cygwin_root as optional argument; tuned;
2013-04-29 blanchet 2013-04-29 use record instead of big tuple
2013-04-29 wenzelm 2013-04-29 clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
2013-04-29 blanchet 2013-04-29 merge
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 removed unreferenced thm
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 code tuning
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 nipkow 2013-04-29 tuned
2013-04-29 traytel 2013-04-29 tuned operator precedence
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-29 nipkow 2013-04-29 tuned
2013-04-29 nipkow 2013-04-29 tuned
2013-04-29 nipkow 2013-04-29 tuned
2013-04-28 nipkow 2013-04-28 tuned
2013-04-27 ballarin 2013-04-27 Clarified confusing sentence in locales tutorial.
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;