[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
begin

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 = ???"
  sorry

end

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?

Thanks.

Best regards,
Iulia Dragomir


-- 
Iulia Dragomir, Ph.D.
Aalto University School of Science
Department of Computer Science
PO Box 15400
FI-00076 Aalto
Finland
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.