# HG changeset patch
# User wenzelm
# Date 1571148251 -7200
# Node ID dbc82c54f6f0e492b839655182cbc81c4abff151
# Parent  80f3a290b35cdb1cd9ad1538ea5813a03c66c3ef
support for proof terms;

diff -r 80f3a290b35c -r dbc82c54f6f0 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Oct 15 14:14:10 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Oct 15 16:04:11 2019 +0200
@@ -170,6 +170,7 @@
     val CONST = Value("const")
     val AXIOM = Value("axiom")
     val THM = Value("thm")
+    val PROOF = Value("proof")
     val CLASS = Value("class")
     val LOCALE = Value("locale")
     val LOCALE_DEPENDENCY = Value("locale_dependency")