support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);
authorwenzelm
Mon Jun 24 16:26:25 2019 +0200 (4 weeks ago)
changeset 70359470d4f145e4c
parent 70358 a55cfc8566fd
child 70360 03430649a7d2
support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);
src/Pure/pure_thy.scala
     1.1 --- a/src/Pure/pure_thy.scala	Sun Jun 23 13:42:16 2019 +0000
     1.2 +++ b/src/Pure/pure_thy.scala	Mon Jun 24 16:26:25 2019 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  
     1.5  object Pure_Thy
     1.6  {
     1.7 +  /* Pure logic */
     1.8 +
     1.9    val DUMMY: String = "dummy"
    1.10    val FUN: String = "fun"
    1.11    val PROP: String = "prop"
    1.12 @@ -17,4 +19,18 @@
    1.13    val ALL: String = "Pure.all"
    1.14    val IMP: String = "Pure.imp"
    1.15    val EQ: String = "Pure.eq"
    1.16 +
    1.17 +
    1.18 +  /* proof terms (abstract syntax) */
    1.19 +
    1.20 +  val PROOF: String = "proof"
    1.21 +
    1.22 +  val APPT: String = "Appt"
    1.23 +  val APPP: String = "AppP"
    1.24 +  val ABST: String = "Abst"
    1.25 +  val ABSP: String = "AbsP"
    1.26 +  val HYP: String = "Hyp"
    1.27 +  val ORACLE: String = "Oracle"
    1.28 +  val OFCLASS: String = "OfClass"
    1.29 +  val MINPROOF: String = "MinProof"
    1.30  }