src/Pure/name.scala
author wenzelm
Mon, 02 Dec 2024 14:08:28 +0100
changeset 81537 d230683a35fc
parent 80272 9f89b3c41460
permissions -rw-r--r--
more direct Proof_Context.lookup_free -- bypass redundancy of Proof_Context.check_const;
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
}