changeset 69919 | 7837309d633a |
parent 68846 | da0cb00a4d6a |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/Thy/thy_element.scala Sun Mar 17 21:26:42 2019 +0100 +++ b/src/Pure/Thy/thy_element.scala Mon Mar 18 21:05:34 2019 +0100 @@ -30,6 +30,13 @@ case Some((_, qed)) => Iterator(head, qed) } + def proof_start: Option[A] = + proof match { + case None => None + case Some((Nil, qed)) => Some(qed) + case Some((start :: _, _)) => Some(start.head) + } + def last: A = proof match { case None => head