Summary
- nicer error
- more debugging
- more general, reliable N2M
- better warning, with definitions in right order
- export ML function
- added timers to N2M
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) |
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) |
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) |
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) |
The file was modified | src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff) |
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) |