Page MenuHomeIsabelle/Phabricator

Clarify indentation after 'oops'
Open, NormalPublic

Description

The oops command in special in various ways, and can lead to odd indentation in the following example (Isabelle2019):

lemma "A ⟹ B"
  oops

  term C

Event Timeline

makarius triaged this task as Normal priority.Feb 25 2020, 11:52 AM
makarius created this task.