Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. to be able to use the more standard Library/FSet.thy, rather than Quotient_Examples/FSet.thy (patch by Joachim Breitner)
Changeset 6849:c515e20878fe by christian urban _christian dot urban at kcl dot ac dot uk_:
to be able to use the more standard Library/FSet.thy, rather than Quotient_Examples/FSet.thy (patch by Joachim Breitner)
The file was modified thys/Nominal2/Nominal2_Base.thy (diff)
The file was modified thys/Nominal2/ROOT (diff)
The file was modified thys/Nominal2/nominal_library.ML (diff)