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) |