Re: [isabelle] variable in Isar?



You can define constants, both globally (at the level of the theory) and local to a context. To get the meaning of such a constant, you have to refer to its defining equation explicitly. You can also create abbreviations, which are essentially macros in that there is no defining equation because the new symbol always expands to its meaning.

Globally, use keywords such as “definition" and “abbreviation". Local to a context, you can use “def" and “let". More information is available in the documentation.

Larry

On 6 Jul 2012, at 07:43, 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.