src/HOL/Imperative_HOL/Mrec.thy
changeset 41910 709c04e7b703
parent 40671 5e46057ba8e0
child 44890 22f665a2e91c