more operations (as in ML);

--- a/src/Pure/General/value.scala	Tue Dec 11 21:23:02 2018 +0100
+++ b/src/Pure/General/value.scala	Tue Dec 11 23:59:41 2018 +0100
@@ -30,6 +30,12 @@
       catch { case _: NumberFormatException => None }
     def parse(s: java.lang.String): scala.Int =
       unapply(s) getOrElse error("Bad integer: " + quote(s))
+
+    def parse_nat(s: java.lang.String): scala.Int =
+      s match {
+        case Value.Int(n) if n >= 0 => n
+        case _ => error("Bad natural number: " + quote(s))
+      }
   }
 
   object Long