[isabelle] Variable sharing



Hi,

If I have two locales:

locale loc1 =
fixes x::real
assumes "x < 2"

locale loc2 =
fixes y::real
assumes "y < 3"

is there a way to define a proof goal for showing EX x. x < 2 in loc1
*and* EX x. x < y in loc2 (as one proof goal)? Does this require some
form of variable sharing?

Thanks
John





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