src/HOL/IMPP/Hoare.ML
changeset 9973 d048e08f3347
parent 9078 b8780970d0ed
child 10834 a7897aebbffc