src/HOL/Hoare/ROOT.ML
changeset 14024 213dcc39358f
parent 13875 12997e3ddd8d
child 14028 ff6eb32b30a1