title: What does depth refer to in Isar Virtual Machine output?
body: <p>Here is a proof:</p>
  
  <pre><code>theory Example
  
  imports Main
  
  begin
  
  datatype natural = Zero | Succ natural
  
  lemma "⋀ n. n = Succ m ⟹ n ≠ Zero"
  proof -
   fix n
   assume "n = Succ m" 
   from this show "n ≠ Zero" by (metis natural.distinct(2))
  qed
  
  end
  </code></pre>
  
  <p>The <code>depth</code> value is 0 throughout the proof but after </p>
  
  <pre><code>show "n ≠ Zero"
  </code></pre>
  
  <p>it changes to </p>
  
  <pre><code>proof (prove): depth 1
  </code></pre>
  
  <p>What does <code>depth</code> mean here? Is it any important when carrying out a proof?</p>