![[Jenkins]](/jenkins/static/51af4dc4/images/svgs/logo.svg){kind=logo}
Summary
- Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
| The file was added | src/HOL/IMP/Hoare_Total_EX2.thy |
| The file was added | src/HOL/IMP/VCG_Total_EX2.thy |
| The file was modified | src/HOL/IMP/Abs_Int3.thy (diff) |
| The file was modified | src/HOL/IMP/Big_Step.thy (diff) |
| The file was modified | src/HOL/IMP/Compiler2.thy (diff) |
| The file was modified | src/HOL/IMP/Denotational.thy (diff) |
| 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/IMP/Live_True.thy (diff) |
| The file was modified | src/HOL/IMP/VCG_Total_EX.thy (diff) |
| The file was modified | src/HOL/ROOT (diff) |