src/HOL/Isar_examples/HoareEx.thy
changeset 16007 4dcccaa11a13
parent 15912 47aa1a8fcdc9
child 16417 9bc16273c2d4