[isabelle] Accessing ML terms in Isabelle theory

Dear all,

I would like to ask if and how it is possible to refer in an Isabelle
theory to an ML defined term. For example, I have the following theory:

theory Test imports Main

definition "A a b = a + b"

ML {*
  val t1 = "a + b";
  val t2 = @{cterm "a+b"};
  val t3 = @{term "a + b"};

lemma "A a b = ???"


Particularly, how can I use one of the three t's as the right hand-side
member of the lemma? And which t - string t1, cterm t2 or term t3 -
should be used in this case?


Best regards,
Iulia Dragomir

Iulia Dragomir, Ph.D.
Aalto University School of Science
Department of Computer Science
PO Box 15400
FI-00076 Aalto
Email: iulia.dragomir at aalto.fi
Phone: +358 503 872710
Web: http://users.ics.aalto.fi/iulia

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