src/HOL/IMP/VC.ML
1996-01-23 nipkow 1996-01-23 Added vcwp
1996-01-23 nipkow 1996-01-23 Added a verified verification-condition generator.