doc-src/TutorialI/Overview/RECDEF.thy
changeset 12899 7d5b690253ee
parent 12815 1f073030b97a
child 13238 a6cb18a25cbb
equal deleted inserted replaced
12898:c78872ea3320 12899:7d5b690253ee