src/HOL/Imperative_HOL/Mrec.thy
changeset 45478 8e299034eab4
parent 44890 22f665a2e91c