Pure theory content;
authorwenzelm
Fri, 03 Aug 2018 14:08:33 +0200
changeset 68713 fb44580680c4
parent 68712 fc51dcb4e6fd
child 68714 1d5ab386eaf0
Pure theory content;
src/Pure/build-jars
src/Pure/pure_thy.scala
--- a/src/Pure/build-jars	Thu Aug 02 22:24:16 2018 +0200
+++ b/src/Pure/build-jars	Fri Aug 03 14:08:33 2018 +0200
@@ -159,6 +159,7 @@
   Tools/update_then.scala
   Tools/update_theorems.scala
   library.scala
+  pure_thy.scala
   term.scala
   term_xml.scala
   ../Tools/Graphview/graph_file.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/pure_thy.scala	Fri Aug 03 14:08:33 2018 +0200
@@ -0,0 +1,19 @@
+/*  Title:      Pure/pure_thy.scala
+    Author:     Makarius
+
+Pure theory content.
+*/
+
+package isabelle
+
+
+object Pure_Thy
+{
+  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"
+}