Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Launchbury: Use notation instead of repeated abbreviation when trying to use notation coming from a locale. Also, replace use of @{abbrev …} by @{term …}, as abbrev is no longer happy here.
Changeset 6828:4ce016f2e370 by joachim breitner _mail@joachim-breitner.de_:
Launchbury: Use notation instead of repeated abbreviation<br><br>when trying to use notation coming from a locale. Also, replace use of<br>@{abbrev …} by @{term …}, as abbrev is no longer happy here.
The file was modified thys/Launchbury/AbstractDenotational.thy (diff)
The file was modified thys/Launchbury/Denotational.thy (diff)
The file was modified thys/Launchbury/EverythingAdequacy.thy (diff)
The file was modified thys/Launchbury/ResourcedDenotational.thy (diff)