src/Pure/name.scala
author wenzelm
Fri, 07 Jun 2024 23:53:31 +0200
changeset 80295 8a9588ffc133
parent 80272 9f89b3c41460
permissions -rw-r--r--
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
80270
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/name.scala
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     3
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     4
Items with formal name.
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     5
*/
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     6
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     7
package isabelle
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     8
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
     9
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
    10
object Name {
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
    11
  trait T { def name: String }
80272
9f89b3c41460 clarified signature;
wenzelm
parents: 80270
diff changeset
    12
9f89b3c41460 clarified signature;
wenzelm
parents: 80270
diff changeset
    13
  type Data[A] = Map[String, A]
80270
1d4300506338 clarified signature;
wenzelm
parents:
diff changeset
    14
}