Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. nicer error
  2. more debugging
  3. more general, reliable N2M
  4. better warning, with definitions in right order
  5. export ML function
  6. added timers to N2M
Changeset 62690:c4fad0569a24 by blanchet:
nicer error
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lift.ML (diff)
Changeset 62689:9b8b3db6ac03 by blanchet:
more debugging
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
Changeset 62688:a3cccaef566a by blanchet:
more general, reliable N2M
The file was modified src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML (diff)
Changeset 62687:1c4842b32bfb by blanchet:
better warning, with definitions in right order
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML (diff)
Changeset 62686:6e8924f957f6 by blanchet:
export ML function
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
Changeset 62685:1e5cf471e703 by blanchet:
added timers to N2M
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)