Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. added new vcg based on existentially quantified while-rule
Changeset 63538:d7b5e2a222c2 by nipkow:
added new vcg based on existentially quantified while-rule
The file was addedsrc/HOL/IMP/VCG_Total_EX.thy
The file was modified src/HOL/IMP/Hoare_Sound_Complete.thy (diff)
The file was modified src/HOL/IMP/Hoare_Total.thy (diff)
The file was modified src/HOL/IMP/Hoare_Total_EX.thy (diff)
The file was modified src/HOL/ROOT (diff)