doc-src/Tutorial/Recdef/constsgcd
author paulson
Mon, 24 Nov 2003 15:33:07 +0100
changeset 14266 08b34c902618
parent 6100 40d66bc3e83f
permissions -rw-r--r--
conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field

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