support for proof terms;
authorwenzelm
Tue, 15 Oct 2019 16:04:11 +0200
changeset 70882 dbc82c54f6f0
parent 70881 80f3a290b35c
child 70883 93767b7a8e7b
support for proof terms;
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")