[isabelle] The environment function



Attachment: WLG.thy
Description: Binary data

How i can define an “env” function in the theory attached here , 
in such way that if i do the following 
value "evalExp (Var 1 ) env” 

the output will for example 
“5”
	:: "int"


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