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?

I don't really understand what it is that you want. Can you clarify again?

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>`

.

@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>?

(Misunderstood question, deleting unhelpful answer)

(Misunderstood question, deleting unhelpful answer)

I don't understand what you mean by ‘verbatim environment’ and I also don't understand what you mean by ‘toolchain’.

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”.

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.

@Manuel Eberl verbatim environment: \begin{verbatim} LaTeX environment in a text < > block in an Isabelle theory file.

toolchain: the Isabelle document preparation toolchain.

(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)

Ah, you mean you want to be able to write ∀ in an Isabelle text block and get the corresponding LaTeX character?

Try putting the symbols in cartouches

Indeed

```
text ‹
Foo ‹∀x. P x ⟶ Q x› Bar
›
```

That should work

@Manuel Eberl it did the trick (with \tt):

Thanks indeed.

It took me a while to realise you were talking about the LaTeX output

Sorry for not being clear

No worries!

Last updated: Sep 25 2022 at 23:25 UTC