doc-src/TutorialI/Recdef/termination.thy
changeset 31795 be3e1cc5005c
parent 19593 c52a4360a41d
equal deleted inserted replaced
31794:71af1fd6a5e4 31795:be3e1cc5005c