doc-src/Tutorial/Recdef/end
author paulson
Fri, 21 May 1999 10:47:07 +0200
changeset 6674 32892a8ecb15
parent 6100 40d66bc3e83f
permissions -rw-r--r--
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)

end