doc-src/TutorialI/Recdef/examples.thy
changeset 43627 ecd4bb7a8bc0
parent 16417 9bc16273c2d4
equal deleted inserted replaced
43626:a867ebb12209 43627:ecd4bb7a8bc0