src/Pure/Thy/thy_header.scala
author haftmann
Tue, 24 Nov 2009 17:28:25 +0100
changeset 33955 fff6f11b1f09
parent 32466 a393b7e2a2f8
child 34169 7501b2910900
permissions -rw-r--r--
curried take/drop
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/thy_header.scala
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     3
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     4
Theory header keywords.
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     5
*/
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     6
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     7
package isabelle
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     8
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     9
32466
a393b7e2a2f8 modernized Thy_Header;
wenzelm
parents: 32450
diff changeset
    10
object Thy_Header
32450
375db037f4d2 misc tuning;
wenzelm
parents: 29140
diff changeset
    11
{
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    12
  val HEADER = "header"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    13
  val THEORY = "theory"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    14
  val IMPORTS = "imports"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    15
  val USES = "uses"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    16
  val BEGIN = "begin"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    17
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    18
  val keywords = List("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    19
}