[isabelle] Unexpected assumptions in nested contexts



Nesting two contexts, where the inner context makes assumptions about
fixed variables from the outer context, results in unexpected
all-quantified assumptions. Consider this minimal example:

context
  fixes I :: "'a set"
begin

  context
    assumes I: "finite I"
  begin
    lemma test: "something_about I"
    sorry
  end

end

Looking at the fact `test` from outside both contexts with `thm test`, I
get:

(!!I. finite I) ==> ?something_about ?I  [!]

Obviously, this fact says something completely different. Am I doing
something wrong here?

(Also, what does the `[!]` mean after the fact?)






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