[isabelle] Proving relationships between locale predicates.


I've got two locales A (with predicate "A x") and B and

  sublocale A <= B (f x)

holds. Now, if I have "A x", how can I show "B (f x)" without repeating the proof for the sublocale property?

I only need one lemma from B, so I would really like to avoid instantiating A, as this takes very long (around 2.5s per instantiation).

  -- Lars

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