Josh Chen (May 26 2020 at 19:41): Josh Chen (May 26 2020 at 19:41):Is there a binding to get locale assumptions internally? So if I have e.g.
locale my_loc =
fixes A
assumes "pred A"
begin
lemma my_lem:
notes ???
...
what do I write for ??? in order to refer to "pred A"?
Kevin Kappelmann (May 26 2020 at 19:52):Is this what you are looking for?
locale my_loc =
fixes A
assumes my_asm: "pred A"
begin
lemma my_lem:
notes my_asm
Yeah that's what I do. Just wondering if there is a predefined name. Thanks!
Kevin Kappelmann (May 26 2020 at 19:57):What happens if you put print_theorems below begin?
Kevin Kappelmann (May 26 2020 at 19:59):Seems like you could quote my_loc_def, which of course I would not recommend ^^
Last updated: Dec 21 2024 at 16:20 UTC