doc-src/Tutorial/Ifexpr/normal_norm.ML
author paulson
Fri, 26 May 2000 18:04:17 +0200
changeset 8983 15bd7d568fb2
parent 5377 efb799c5ed3c
permissions -rw-r--r--
named the primrec clauses of upt

Goal "normal(norm b)";