src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
2013-06-06 blanchet 2013-06-06 renamed ML variables
2013-06-06 blanchet 2013-06-06 tuned record field names to avoid confusion between low-level and high-level constants/theorems
2013-06-06 blanchet 2013-06-06 tuned signature
2013-06-06 blanchet 2013-06-06 support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
2013-06-06 blanchet 2013-06-06 tuned ML variable names
2013-06-05 blanchet 2013-06-05 tuning
2013-06-05 blanchet 2013-06-05 avoid code duplication
2013-06-05 blanchet 2013-06-05 eliminated dead argument
2013-06-05 blanchet 2013-06-05 one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")
2013-06-05 blanchet 2013-06-05 tuning
2013-06-05 blanchet 2013-06-05 simpler, more robust iterator goal construction code
2013-06-05 blanchet 2013-06-05 tuning
2013-06-05 blanchet 2013-06-05 reverted 23929f647f79 -- not needed after all
2013-06-05 blanchet 2013-06-05 killed dead code
2013-06-05 blanchet 2013-06-05 tuning
2013-06-05 blanchet 2013-06-05 slightly nicer ML interface
2013-06-05 blanchet 2013-06-05 added convenience function
2013-06-05 blanchet 2013-06-05 keep a record of the fixpoint equations
2013-06-05 blanchet 2013-06-05 export ML function (needed for "primrec_new")
2013-06-04 blanchet 2013-06-04 export ML function
2013-05-29 blanchet 2013-05-29 tuning
2013-05-29 blanchet 2013-05-29 more work on general recursors
2013-05-29 blanchet 2013-05-29 tuning (use lists rather than pairs of lists throughout)
2013-05-29 blanchet 2013-05-29 generalized recursors, effectively reverting inductive half of c7a034d01936
2013-05-29 blanchet 2013-05-29 tuning
2013-05-28 blanchet 2013-05-28 tuning (refactoring)
2013-05-28 blanchet 2013-05-28 refactored triplicated functionality
2013-05-28 blanchet 2013-05-28 tuning -- avoided unreadable true/false all over the place for LFP/GFP
2013-05-28 blanchet 2013-05-28 exported ML function
2013-05-28 blanchet 2013-05-28 clean up list of theorems
2013-05-27 blanchet 2013-05-27 tuning
2013-05-27 blanchet 2013-05-27 killed dead argument
2013-05-27 blanchet 2013-05-27 tuning
2013-05-27 blanchet 2013-05-27 generalized "mk_co_iter" to handle mutualized (co)iterators
2013-05-27 blanchet 2013-05-27 tuning
2013-05-07 blanchet 2013-05-07 removed dead argument
2013-05-07 blanchet 2013-05-07 more robust iterator construction (needed for mutualized FPs)
2013-05-07 blanchet 2013-05-07 tuning
2013-05-07 blanchet 2013-05-07 removed tracing
2013-05-07 blanchet 2013-05-07 export one more function
2013-05-07 blanchet 2013-05-07 added field to record
2013-05-07 blanchet 2013-05-07 tuning
2013-05-07 blanchet 2013-05-07 removed dead code
2013-05-07 blanchet 2013-05-07 move function to library
2013-05-07 blanchet 2013-05-07 tuning
2013-05-07 blanchet 2013-05-07 tuning
2013-05-07 blanchet 2013-05-07 code tuning
2013-05-07 blanchet 2013-05-07 refactoring
2013-05-07 blanchet 2013-05-07 export one more function + tuning
2013-05-07 blanchet 2013-05-07 tuned names + extended ML signature
2013-05-07 blanchet 2013-05-07 tuning
2013-05-07 blanchet 2013-05-07 imported patch refactor_coiter_constr
2013-05-06 blanchet 2013-05-06 started factoring out coiter construction
2013-05-06 blanchet 2013-05-06 rationalize ML signature
2013-05-06 blanchet 2013-05-06 factor out construction of iterator
2013-05-06 blanchet 2013-05-06 tuning
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