1/* Title: Pure/pure_thy.scala 2 Author: Makarius 3 4Pure theory content. 5*/ 6 7package isabelle 8 9 10object Pure_Thy 11{ 12 /* Pure logic */ 13 14 val DUMMY: String = "dummy" 15 val FUN: String = "fun" 16 val PROP: String = "prop" 17 val ITSELF: String = "itself" 18 19 val ALL: String = "Pure.all" 20 val IMP: String = "Pure.imp" 21 val EQ: String = "Pure.eq" 22 val TYPE: String = "Pure.type" 23 24 25 /* abstract syntax for proof terms */ 26 27 val PROOF: String = "Pure.proof" 28 29 val APPT: String = "Pure.Appt" 30 val APPP: String = "Pure.AppP" 31 val ABST: String = "Pure.Abst" 32 val ABSP: String = "Pure.AbsP" 33 val HYP: String = "Pure.Hyp" 34 val ORACLE: String = "Pure.Oracle" 35 val OFCLASS: String = "Pure.OfClass" 36 val MINPROOF: String = "Pure.MinProof" 37} 38