Re: [isabelle] Variable sharing
locale loc1 =
assumes "x < 2"
locale loc2 =
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?
You need to define a context (ie locale) that inherits from both.
This can be achieved with locale expressions. I recommend reading the
Section 6. Sharing is achieved by providing suitable locale
instances. In your example, there is no sharing (Parameters x and y
This archive was generated by a fusion of
Pipermail (Mailman edition) and