title: type_synonym vs consts in Isabelle definition
body: <p>I have the two following expressions in isabelle:</p>
  
  <pre><code>consts drives ::"(Person × Car) set"
  
  type_synonym drives="(Person × Car) set"
  </code></pre>
  
  <p>How they are different in terms of their semantics?</p>
  
  <p>I think that <strong>type_synonym</strong> is just a brief name for the type specified in front of it. right?</p>
  
  <p>But what <strong>const</strong> is for? (Isabelle tutorial document --page 119-- says: "This is Isabelle’s way of declaring a constant without defining it." But in what sense above expression can be a constant?!!)</p>
  
  <p>Thanks</p>