Entry	Value
Package Name	list-nub-def
Count	3
Theorems	nub_def : !l. nub l = REVERSE (setify (REVERSE l)) setify_cons : !h t. setify (CONS h t) = (if MEM h t then setify t else CONS h (setify t)) setify_nil : setify [] = []

Back to main package page