src/HOL/Imperative_HOL/Imperative_HOL.thy
changeset 42505 fef9a94706c2
parent 37776 df0350f1e7f2
child 53109 186535065f5c