changeset 2541 | 70aa00ed3025 |
parent 2393 | 651fce76c86c |
child 2608 | 450c9b682a92 |
--- 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)"