Gergely Buday (Jan 05 2021 at 08:52): Gergely Buday (Jan 05 2021 at 08:52):I would like to copy theorem output into e-mail. I tried two ways, none of them worked properly.
First: copy from the generated pdf:
[x1 ⇒ x2;
V s. P (SKIP, s) s; V x a s. P (x ::= a, s) (s(x := aval a s));
V c
1 s 1 s 2 c 2 s 3 .
Here and in Thunderbird the meta universal quantifier appears as a capital form of disjunction.
Second: copy from Isabelle/JEdit Output window:
?x1.0 ⇒ ?x2.0 ⟹
(⋀s. ?P (SKIP, s) s) ⟹
(⋀x a s. ?P (x ::= a, s) (s(x := aval a s))) ⟹
(⋀c⇩1 s⇩1 s⇩2 c⇩2 s⇩3. (c⇩1, s⇩1) ⇒ s⇩2 ⟹ ?P (c⇩1, s⇩1) s⇩2 ⟹ (c⇩2, s⇩2) ⇒ s⇩3 ⟹ ?P (c⇩2, s⇩2) s⇩3 ⟹ ?P (c⇩1;; c⇩2, s⇩1) s⇩3) ⟹
instead of $c_1$, c⇩1 appears. Also, x1 becomes ?x1.0 .
Is there a panacea for this?
Mathias Fleury (Jan 05 2021 at 09:19):IIRC, copy-pasting from the HTML preview works
Gergely Buday (Jan 05 2021 at 09:27):This is a generated theorem that is not present in the HTML preview.
Gergely Buday (Jan 05 2021 at 13:18):#!/bin/bash
sed -e $'s/⇩1/\u2081/g' <$1 | \
sed -e $'s/⇩2/\u2082/g' | \
sed -e $'s/⇩3/\u2083/g' | \
sed -e $'s/⇩4/\u2084/g' | \
sed -e $'s/⇩5/\u2085/g' | \
sed -e 's/?//'g
Creates proper subscript numbers up to 5 and removes question marks for schematic variables. This processes theorems in the Output window of Isabelle/JEdit.
Notice the leading $ that enables shell escapes for unicode characters:
Manuel Eberl (Jan 05 2021 at 13:40):you can also do thm [no_vars] to get rid of schematic variables.
Gergely Buday (Jan 05 2021 at 13:51):@Manuel Eberl Does that work only in document preparation's @{thm } sequence or also in Isabelle/JEdit Output window?
I could not add [no_vars] anyhow into
lemmas big_step_induct = big_step.induct [split_format(complete)]
Manuel Eberl (Jan 05 2021 at 13:55):Well you should only use this for presentation, really. You know, when you want to copy-paste stuff into an email or something.
Manuel Eberl (Jan 05 2021 at 13:55):But yes, no_vars is just an attribute. You can do thm foo[no_avsrs] or lemmas bar = foo[no_vars].
Last updated: Dec 21 2024 at 16:20 UTC