# HG changeset patch
# User wenzelm
# Date 1561386385 -7200
# Node ID 470d4f145e4cb636e9379e51e0d5f1487e0b1f24
# Parent  a55cfc8566fd5f1b9cc40df5e3ccdb3553f6fdab
support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);

diff -r a55cfc8566fd -r 470d4f145e4c src/Pure/pure_thy.scala
--- a/src/Pure/pure_thy.scala	Sun Jun 23 13:42:16 2019 +0000
+++ b/src/Pure/pure_thy.scala	Mon Jun 24 16:26:25 2019 +0200
@@ -9,6 +9,8 @@
 
 object Pure_Thy
 {
+  /* Pure logic */
+
   val DUMMY: String = "dummy"
   val FUN: String = "fun"
   val PROP: String = "prop"
@@ -17,4 +19,18 @@
   val ALL: String = "Pure.all"
   val IMP: String = "Pure.imp"
   val EQ: String = "Pure.eq"
+
+
+  /* proof terms (abstract syntax) */
+
+  val PROOF: String = "proof"
+
+  val APPT: String = "Appt"
+  val APPP: String = "AppP"
+  val ABST: String = "Abst"
+  val ABSP: String = "AbsP"
+  val HYP: String = "Hyp"
+  val ORACLE: String = "Oracle"
+  val OFCLASS: String = "OfClass"
+  val MINPROOF: String = "MinProof"
 }