src/HOL/Imperative_HOL/Mrec.thy
changeset 39749 fa94799e3a3b
parent 37792 ba0bc31b90d7
child 39754 150f831ce4a3