src/Doc/Tutorial/Inductive/AB.thy
changeset 80463 3490a9c96d2f
parent 76987 4c275405faae