src/HOL/Nat.thy
changeset 2541 70aa00ed3025
parent 2393 651fce76c86c
child 2608 450c9b682a92
     1.1 --- a/src/HOL/Nat.thy	Thu Jan 23 12:42:07 1997 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Jan 23 12:55:31 1997 +0100
     1.3 @@ -60,11 +60,6 @@
     1.4     "2"  == "Suc 1"
     1.5    "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
     1.6  
     1.7 -(*
     1.8 -syntax (symbols)
     1.9 -
    1.10 -  "LEAST "	:: [idts, bool] => nat		("(3\\<mu>_./ _)" [0, 10] 10)
    1.11 -*)
    1.12  
    1.13  defs
    1.14    Zero_def      "0 == Abs_Nat(Zero_Rep)"