Skip to content
Failed

Changes

Summary

  1. merged
  2. added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image
  3. clarified names;
  4. sketch & explore: TODO comments are addressed in parent commits
  5. sketch & explore: reduce unnecessary type constraints
  6. sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
  7. sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
  8. change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible);
Changeset 79906:e6f0a93e2edd by desharna:
merged
Changeset 79905:1f509d01c9e3 by desharna:
added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 79904:1cfc913987d9 by wenzelm:
clarified names;
The file was modified src/Pure/Build/build_process.scala (diff)
The file was modified src/Pure/Build/build_schedule.scala (diff)
Changeset 79903:d3811cf07da6 by simon wimmer _wimmers@in.tum.de_:
sketch & explore: TODO comments are addressed in parent commits
The file was modified src/HOL/ex/Sketch_and_Explore.thy (diff)
Changeset 79902:0d5c41ea208a by simon wimmer _wimmers@in.tum.de_:
sketch & explore: reduce unnecessary type constraints
The file was modified src/HOL/ex/Sketch_and_Explore.thy (diff)
Changeset 79901:54e9875e491f by simon wimmer _wimmers@in.tum.de_:
sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
The file was modified src/HOL/ex/Sketch_and_Explore.thy (diff)
Changeset 79900:8f0ff2847ba8 by simon wimmer _wimmers@in.tum.de_:
sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
The file was modified src/HOL/ex/Sketch_and_Explore.thy (diff)
Changeset 79899:c73a36081b1c by fabian huch _huch@in.tum.de_:
change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible);
The file was modified src/Pure/Build/build_benchmark.scala (diff)