pGCL for Isabelle
This Isabelle theory package provides a mechanisation of McIver and Morgan's Probabilistic Guarded Command Language (pGCL). This package is now in the archive of formal proofs, which should be considered the canonical version (and is guaranteed to work with the current release of Isabelle/HOL. This page hosts historical and development versions only.