Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Automated merge with https://bitbucket.org/isa-afp/afp-devel
  2. Weakened interface condition for successors function & added PR_CONST to refinement thms
  3. Automated merge with https://bitbucket.org/isa-afp/afp-devel
  4. merged
  5. frame_step_tac always normalizes
Changeset 7249:1efcfe4e28ad by simon wimmer _wimmers@in.tum.de_:
Automated merge with https://bitbucket.org/isa-afp/afp-devel
Changeset 7248:3f9579cc6bd6 by simon wimmer _wimmers@in.tum.de_:
Weakened interface condition for successors function & added PR_CONST to refinement thms
The file was modified thys/Refine_Imperative_HOL/Examples/Worklist_Subsumption.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Examples/Worklist_Subsumption_Impl.thy (diff)
Changeset 7247:eab2a778fbaa by simon wimmer _wimmers@in.tum.de_:
Automated merge with https://bitbucket.org/isa-afp/afp-devel
Changeset 7246:30d2f96d703c by simon wimmer _wimmers@in.tum.de_:
merged
Changeset 7245:86f6ce0ecb8d by simon wimmer _wimmers@in.tum.de_:
frame_step_tac always normalizes
The file was modified thys/Refine_Imperative_HOL/Sepref_Frame.thy (diff)