Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [isabelle-dev] print_theorems uses a wrong con...

view this post on Zulip Email Gateway (Aug 19 2022 at 11:55):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Ondřej,

print_theorems always prints the newly emerged theorems in the
background context – try e.g.

context comm_monoid
begin

lemma foo: "x = x" ..

print_theorems

end

I confess the reference manual is not very explicit on this.

Cheers,
Florian
signature.asc

Last updated: Apr 23 2024 at 08:19 UTC