Packages

object BelleLabels

Default labels used by the KeYmaera X tactics. Other labels can be used by the user, but this list of labels makes it easier to match.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. BelleLabels
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val QECEX: BelleLabel
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  7. val commitTx: BelleLabel

    Commit a label transaction started with startTx.

    Commit a label transaction started with startTx.

    label(startTx) & doStuffThatCreatesLabels & label(commitTx)
  8. val cutShow: BelleLabel
  9. val cutUse: BelleLabel
  10. val dIInit: BelleLabel
  11. val dIStep: BelleLabel
  12. val dVderiv: BelleLabel
  13. val dVexists: BelleLabel
  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  16. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  17. val fixUseCase: BelleLabel
  18. val fixpoint: BelleLabel
  19. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  20. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  21. val indStep: BelleLabel
  22. val initCase: BelleLabel
  23. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  24. def lemmaUnproved(name: String): BelleLabel
  25. val mrShow: BelleLabel
  26. val mrUse: BelleLabel
  27. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  28. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  29. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  30. def replaceTxWith(l: BelleLabel): BelleLabel

    Shorthand for rollback, insert label, commit.

  31. val rollbackTx: BelleLabel

    Rollback a label transaction started with startTx; rollback should be followed immediately by a label.

    Rollback a label transaction started with startTx; rollback should be followed immediately by a label.

    label(startTx) & doStuffThatCreatesLabels & label(rollbackTx) & label(useCase)
  32. val startTx: BelleLabel

    Starts a label transaction

  33. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  34. def toString(): String
    Definition Classes
    AnyRef → Any
  35. val useCase: BelleLabel
  36. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  37. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  38. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped