equal
deleted
inserted
replaced
211 session "HOL-Hoare" in Hoare = HOL + |
211 session "HOL-Hoare" in Hoare = HOL + |
212 description {* |
212 description {* |
213 Verification of imperative programs (verification conditions are generated |
213 Verification of imperative programs (verification conditions are generated |
214 automatically from pre/post conditions and loop invariants). |
214 automatically from pre/post conditions and loop invariants). |
215 *} |
215 *} |
216 |
|
217 theories Hoare |
216 theories Hoare |
218 files "document/root.bib" "document/root.tex" |
217 files "document/root.bib" "document/root.tex" |
219 |
218 |
220 session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL + |
219 session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL + |
221 description {* |
220 description {* |