--- a/src/Pure/thm_name.scala Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/thm_name.scala Fri Apr 01 17:06:10 2022 +0200
@@ -10,10 +10,8 @@
import scala.math.Ordering
-object Thm_Name
-{
- object Ordering extends scala.math.Ordering[Thm_Name]
- {
+object Thm_Name {
+ object Ordering extends scala.math.Ordering[Thm_Name] {
def compare(thm_name1: Thm_Name, thm_name2: Thm_Name): Int =
thm_name1.name compare thm_name2.name match {
case 0 => thm_name1.index compare thm_name2.index
@@ -32,8 +30,7 @@
}
}
-sealed case class Thm_Name(name: String, index: Int)
-{
+sealed case class Thm_Name(name: String, index: Int) {
def print: String =
if (name == "" || index == 0) name
else name + "(" + index + ")"