[isabelle] Variable sharing


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?


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