Email Gateway (Aug 18 2022 at 14:49): Email Gateway (Aug 18 2022 at 14:49):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users,
I have tried to use I3P, but there are some principal problems.
First, if I type, for example, ==>, the system types some square symbol... Istallation "Isabelle Text" and choosing it as a font (in Tools > Options > Fonts) did not help, ans I did not notice any reaction at all.
Aften this, I wanted to turn off Unicode Tokens at all (In Emacs Proof General I can choose Proof General > Options > Unicode Tokens to turn off), but I did not find a way how to do this.
In general, it is hard to find the analogy for most of commands from Proof General Menue. For example, I often use sledgehammer (Isabeele > Commands > Sledgehammer), show and hide types (Isabelle > Settings > Show types), do search (Proof general > Find theorems), etc. Some of this actions (like search in the whole library) are crutial. How to do the same in I3P?
Sincerely,
Bogdan.
Last updated: Apr 25 2024 at 20:15 UTC