diff -r ba8311047f18 -r 70aa00ed3025 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Jan 23 12:42:07 1997 +0100
+++ b/src/HOL/Nat.thy	Thu Jan 23 12:55:31 1997 +0100
@@ -60,11 +60,6 @@
    "2"  == "Suc 1"
   "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
 
-(*
-syntax (symbols)
-
-  "LEAST "	:: [idts, bool] => nat		("(3\\<mu>_./ _)" [0, 10] 10)
-*)
 
 defs
   Zero_def      "0 == Abs_Nat(Zero_Rep)"