Gergely Buday (Aug 10 2020 at 09:58): Gergely Buday (Aug 10 2020 at 09:58):I copied some Coq code into an Isabelle theory file using the verbatim LaTeX environment. The result was this:
Axiom le_antisym : \<forall> x y, x \<le> y \<Rightarrow> y \<le> x \<Rightarrow> x = y.
where le = less or equal sign.
I tried the unicode-math environment suggested here:
https://tex.stackexchange.com/questions/149710/how-to-write-math-symbols-in-a-verbatim
but I guess Isabelle/jEdit already stores the universal quantor as \<forall>.
How can I enter math unicode symbols into the file so that this translation does not occur and I would see these math symbols in their original form?
Manuel Eberl (Aug 10 2020 at 10:04):I don't really understand what it is that you want. Can you clarify again?
Lukas Stevens (Aug 10 2020 at 10:16):Save and then reload the file with F5. The symbols should show up in the unicode form. Note that isabelle does not store its theory files with unicode symbols but replaces them with, e.g. \<forall>.
Gergely Buday (Aug 10 2020 at 10:45):@Manuel Eberl I have ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y. in a verbatim environment but the toolchain typesets it as
\<forall> x y, x \<le> y \<Rightarrow> y \<le> x \<Rightarrow> x = y.
The question is: how can I make Isabelle/jEdit to save my unicode symbols as unicode symbols and not as Isabelle ASCII names like \<forall> and \<Rightarrow>?
Josh Chen (Aug 10 2020 at 10:50):(Misunderstood question, deleting unhelpful answer)
Josh Chen (Aug 10 2020 at 10:51):(Misunderstood question, deleting unhelpful answer)
Manuel Eberl (Aug 10 2020 at 10:55):I don't understand what you mean by ‘verbatim environment’ and I also don't understand what you mean by ‘toolchain’.
Manuel Eberl (Aug 10 2020 at 10:56):If you've ended up with \<Rightarrow> in jEdit somehow and want to get the Unicode display back, try "File → Reload" or, if that doesn't work, "File → Reload with Encoding → UTF-8-Isabelle”.
Manuel Eberl (Aug 10 2020 at 10:57):The actual saved file will always contain the expanded ASCII notation (e.g. \<Rightarrow>) and there's not really a way to prevent that, I think. If you do want to get this text, you can of course always just open the file with Isabelle/jEdit and copy out the text as it is displayed there.
Gergely Buday (Aug 10 2020 at 10:58):@Manuel Eberl verbatim environment: \begin{verbatim} LaTeX environment in a text < > block in an Isabelle theory file.
toolchain: the Isabelle document preparation toolchain.
Manuel Eberl (Aug 10 2020 at 10:58):(Makarius doesn't like Unicode as a format for actually saving Isabelle source due to several issues such as normalisation and some other reasons I don't remember)
Manuel Eberl (Aug 10 2020 at 10:58):Ah, you mean you want to be able to write ∀ in an Isabelle text block and get the corresponding LaTeX character?
Manuel Eberl (Aug 10 2020 at 10:59):Try putting the symbols in cartouches
Gergely Buday (Aug 10 2020 at 10:59):Indeed
Manuel Eberl (Aug 10 2020 at 10:59):text ‹
Foo ‹∀x. P x ⟶ Q x› Bar
›
That should work
Gergely Buday (Aug 10 2020 at 11:17):@Manuel Eberl it did the trick (with \tt):
Thanks indeed.
Manuel Eberl (Aug 10 2020 at 11:23):It took me a while to realise you were talking about the LaTeX output
Gergely Buday (Aug 10 2020 at 11:27):Sorry for not being clear
Manuel Eberl (Aug 10 2020 at 11:34):No worries!
Last updated: Apr 20 2024 at 12:26 UTC