src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
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
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 [mq]: tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 tuning
2013-06-06 blanchet 2013-06-06 avoid duplicate call to "mk_fold_rec_args_types" function
2013-06-06 blanchet 2013-06-06 continuation of f461dca57c66
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