1/*  Title:      Pure/pure_thy.scala
2    Author:     Makarius
3
4Pure theory content.
5*/
6
7package isabelle
8
9
10object Pure_Thy
11{
12  /* Pure logic */
13
14  val DUMMY: String = "dummy"
15  val FUN: String = "fun"
16  val PROP: String = "prop"
17  val ITSELF: String = "itself"
18
19  val ALL: String = "Pure.all"
20  val IMP: String = "Pure.imp"
21  val EQ: String = "Pure.eq"
22  val TYPE: String = "Pure.type"
23
24
25  /* abstract syntax for proof terms */
26
27  val PROOF: String = "Pure.proof"
28
29  val APPT: String = "Pure.Appt"
30  val APPP: String = "Pure.AppP"
31  val ABST: String = "Pure.Abst"
32  val ABSP: String = "Pure.AbsP"
33  val HYP: String = "Pure.Hyp"
34  val ORACLE: String = "Pure.Oracle"
35  val OFCLASS: String = "Pure.OfClass"
36  val MINPROOF: String = "Pure.MinProof"
37}
38