Dear Isabelle-Dev,
this refers to fbf4d50dec91.
Recently I started using interpretation in anonymous contexts to
introduce syntax locally. But now I noticed that print_theorems behaves
differently than I expected.
Consider this example:
context begin
interpretation lifting_syntax .
term "op ===>" -- {* we have the symbol ===> now *}
lemma x: "R ===> R = R ===> R" ..
thm x -- {* everything is OK *}
print_theorems -- {* but print_theorems still outputs fun_rel rather
than ===> *}
end
Best,
Ondrej
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
