Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. (un)folds are not legacy
  2. removed duplicate lemma
  3. derive (co)rec uniformly from (un)fold
Changeset 62907:9ad0bac25a84 by traytel:
(un)folds are not legacy
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML (diff)
Changeset 62906:75ca185db27f by traytel:
removed duplicate lemma
The file was modified src/HOL/BNF_Least_Fixpoint.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_tactics.ML (diff)
Changeset 62905:52c5a25e0c96 by traytel:
derive (co)rec uniformly from (un)fold
The file was addedsrc/HOL/Tools/BNF/bnf_fp_util_tactics.ML
The file was modified src/HOL/BNF_Fixpoint_Base.thy (diff)
The file was modified src/HOL/BNF_Greatest_Fixpoint.thy (diff)
The file was modified src/HOL/BNF_Least_Fixpoint.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)