src/Pure/pure_thy.scala
author wenzelm
Sun, 14 Mar 2021 21:02:34 +0100
changeset 73436 e92f2e44e4d8
parent 71777 3875815f5967
child 75393 87ebf5a50283
permissions -rw-r--r--
removed spurious references to perl / libwww-perl;

/*  Title:      Pure/pure_thy.scala
    Author:     Makarius

Pure theory content.
*/

package isabelle


object Pure_Thy
{
  /* Pure logic */

  val DUMMY: String = "dummy"
  val FUN: String = "fun"
  val PROP: String = "prop"
  val ITSELF: String = "itself"

  val ALL: String = "Pure.all"
  val IMP: String = "Pure.imp"
  val EQ: String = "Pure.eq"
  val TYPE: String = "Pure.type"


  /* abstract syntax for proof terms */

  val PROOF: String = "Pure.proof"

  val APPT: String = "Pure.Appt"
  val APPP: String = "Pure.AppP"
  val ABST: String = "Pure.Abst"
  val ABSP: String = "Pure.AbsP"
  val HYP: String = "Pure.Hyp"
  val ORACLE: String = "Pure.Oracle"
  val OFCLASS: String = "Pure.PClass"
  val MINPROOF: String = "Pure.MinProof"
}