doc-src/TutorialI/Recdef/examples.thy
changeset 9941 fe05af7ec816
parent 9933 9feb1e0c4cb3
child 10362 c6b197ccf1f1
equal deleted inserted replaced
9940:102f2430cef9 9941:fe05af7ec816