[isabelle] values from locales



While studying ~~/doc/locales.pdf, ~~/doc/isar-ref.pdf and and code in Vector_Space.thy I got stuck with evaluating definitions occurring within locale:

  locale lll =
    fixes fff :: "int ⇒ int ⇒ int"
    assumes ccc: "fff a b = fff b a"
  begin
    lemma aaa [code]: "fff a b = a + b"
    sorry
    value "fff 1 2" --{*"fff 1 2" :: "int"  --- EXPECT "3" HERE *}
  end

Question:
What am I missing in order to get

    value "fff 1 2" --{*"3" :: "int"*}

Thanks for patience with this question,
Walther


PS: For pointers into ~~/doc I'd particularly grateful.

Attachment: Locale_Value.thy
Description: application/extension-thy



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