src/HOL/Library/Suc_Notation.thy
changeset 82735 5d0d35680311
parent 81811 76cb80f9637e