[isabelle] add_assoc, add.assoc and reflection



Looking at

   val ctxt = Proof_Context.init_global @{theory Main};
   Syntax.read_term ctxt "add_assoc"
      (* = Free ("add_assoc", "'a"): term *)
   Syntax.read_term ctxt "add.assoc"
      (* ERROR: Undefined constant: "add.assoc"*)

is my assumption right, that the latter is considered outer syntax only?
In other words: The latter is NOT considered to become a valid term (i.e. inner syntax) within some context ?

If both questions are answered "yes", then this question comes up: How comes that the designers of Isabelle are sure, that theorem names never shall occur in functions defined within Isabelle's function package (where function definitions are terms, i.e. belong to inner syntax) ?

And how does that design decision relate to the announcement of "Eisbach, a new sub-language for Isabelle which allows users to write automated reasoning techniques with high-level syntax, avoiding the necessity of descending into ML"?

Walther




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.