title: Can I define multiple names for a theorem?
body: <p>Suppose I have a theorem:</p>
  
  <pre><code>theorem non_ASCII_thm_name:
    "True"
    by simp
  </code></pre>
  
  <p>I want to define an ASCII name for <code>non_ASCII_thm_name</code> with something like the <code>notation</code> command. For example, like this:</p>
  
  <pre><code>notation non_ASCII_thm_name ("ASCII_thm_name")
  </code></pre>
  
  <p>The Isar commands <code>notation</code> and <code>abbreviation</code> can only be used with constants. Is there an Isar command that allows me to to this?</p>
  
  <p>Preferably, all I want my Isar command to provide is a synonym. For example, if I use <code>sledgehammer</code>, it would be preferable that there exist only one theorem, <code>non_ASCII_thm_name</code>, so that <code>sledgehammer</code> is not using an additional fact <code>ASCII_thm_name</code>.</p>