Re: [isabelle] Locale import

locale B = fixes g :: "'b => 'a"
  assumes A: "A (g b)"
  and ...

Contrary to my previous message, this is, of course, well-defined. b is here universally quantified in the assumption. I am still at loss what you are trying to achieve, though.


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