Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. fine-tuned simpset for proving that automatically generated show functions satisfy show law (this should resolve a problem reported by Fabian Immler that success of 'derive "show" ...' sometimes depends on argument order of constructors)
Changeset 8588:ff2ae1f38b5e by Christian Sternagel:
fine-tuned simpset for proving that automatically generated show functions<br>satisfy show law (this should resolve a problem reported by Fabian Immler that<br>success of &#039;derive &quot;show&quot; ...&#039; sometimes depends on argument order of<br>constructors)
The file was modified thys/Show/show_generator.ML (diff)