# HG changeset patch
# User wenzelm
# Date 854020531 -3600
# Node ID 70aa00ed30250d62247e172d900b8d7e9811dac5
# Parent  ba8311047f18295bf2fc8de7d0c1bc8a0ab6478f
removed \<mu> syntax;

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)"