src/HOL/Induct/SList.thy
changeset 36811 4ab4aa5bee1c
parent 35247 0831bd85eee5
child 39246 9e58f0499f57
equal deleted inserted replaced
36810:d9a51339746e 36811:4ab4aa5bee1c