src/Tools/8bit/isa-patches/HOL/Nat.p
author wenzelm
Thu, 15 Feb 2001 17:18:54 +0100
changeset 11145 3e47692e3a3e
parent 1826 2a2c0dbeb4ac
permissions -rw-r--r--
eliminate get_def;

syntax
  "Gmu"	:: (nat => bool) => nat				(binder "´" 10)

translations
  "´x.P"	== "LEAST x. P"