src/HOL/Library/Diagonal_Subsequence.thy
changeset 72572 e7e93c0f6d96
parent 67399 eab6ce8368fa