# Re: [isabelle] variable in Isar?

Dear Gergely,
- inside a proof you can use:
let ?elem = "..."
- in a lemma "heading" you can use:
lemma
defines "elem == ..."
assumes "..."
shows "..."
with corresponding fact "elem_def"
- for a gobal definition you can use the usual "definition" command
- for a non-global definition that might span several lemmas you can use
context
fixes elem
assumes "elem = ..."
begin
...
end

`However, your specific example does not make sense, since it is not
``well-typed. Maybe you wanted to have something like "SOME x. x : {x.
``even x}" (i.e., an arbitrary element from the set "{x. even x}").
`
cheers
chris
On 07/06/2012 03:43 PM, Gergely Buday wrote:

Hi,
is it possible to define a variable in Isar, like
var elem = SOME x. {x. even x}
and then use it later?
- Gergely

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