--- a/src/Pure/thm_name.scala Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm_name.scala Fri Jun 07 23:53:31 2024 +0200
@@ -23,6 +23,8 @@
private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r
+ val empty: Thm_Name = Thm_Name("", 0)
+
def parse(s: String): Thm_Name =
s match {
case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
@@ -31,6 +33,8 @@
}
sealed case class Thm_Name(name: String, index: Int) {
+ def is_empty: Boolean = name.isEmpty
+
def print: String =
if (name == "" || index == 0) name
else name + "(" + index + ")"