[isabelle] about I3P



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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.