src/HOL/Imperative_HOL/Imperative_HOL.thy
changeset 48516 c5d0f19ef7cb
parent 37776 df0350f1e7f2
child 53109 186535065f5c