Summary
- merged
- added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image
- clarified names;
- sketch & explore: TODO comments are addressed in parent commits
- sketch & explore: reduce unnecessary type constraints
- sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
- sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
- change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible);
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Relation.thy (diff) |
The file was modified | src/Pure/Build/build_process.scala (diff) |
The file was modified | src/Pure/Build/build_schedule.scala (diff) |
The file was modified | src/HOL/ex/Sketch_and_Explore.thy (diff) |
The file was modified | src/HOL/ex/Sketch_and_Explore.thy (diff) |
The file was modified | src/HOL/ex/Sketch_and_Explore.thy (diff) |
The file was modified | src/HOL/ex/Sketch_and_Explore.thy (diff) |
The file was modified | src/Pure/Build/build_benchmark.scala (diff) |