How to abort a proof in Isabelle?

I was wondering if there is a way to abort a proof in Isabelle/jEdit?

I searched for commands such as "Reset", "Abort" but couldn't find it.

I know there is Sorry. But I am not sure if one uses Sorry, the theorem at hand is assumed to be true or abandoned. Also, Sorry does not seem to work in the apply..done mode.

Currently, I comment out the theorems that I can't prove. But it requires a lot of typing (four characters each in (* *)) to comment or uncomment something, which is kind of cumbersome.

So is there a standard/universal way to abort a proof in Isabelle?

Solution

First, the command is sorry and it does work (but only) in apply style:

lemma 
  ‹False ∧ True›
  apply (rule conjI)
   apply auto
  sorry

About the actual question, oops aborts proofs, whether in apply style or not:

lemma 
  ‹False ∧ True›
proof -
  have True
    by auto
  oops

An oops-ed proof cannot be referenced later.