doc-src/Tutorial/Recdef/constsgcd
author berghofe
Wed, 07 Aug 2002 16:50:08 +0200
changeset 13471 aed3aef2a0ca
parent 6100 40d66bc3e83f
permissions -rw-r--r--
Removed (now unneeded) declaration of realizer for induction on datatype b.

consts gcd :: "nat*nat => nat"