Custom Query (361 matches)
Results (76 - 78 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #413 | worksforme | Clicking on Find icon does not bring up input buffer | ||
| Description |
This problem may be due to my inexperience with emacs and/or proof general and/or isabelle, but I think at the very least it's a user-friendliness issue. I'm trying to follow the directions in the Isabelle tutorial at http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011/doc/tutorial.pdf in section 3.1.11--Finding Theorems. I load the ToyList.thy that I copied from Figure 2.1, and I process all of the proof commands in that theory. Then I press the "Find" icon. The toolbar changes and the ToyList.thy buffer seems to lose focus, but when I type, no text appears, and I cannot find a buffer that will let me enter my search text. I'm running proof general Version 4.1pre101216 on GNU Emacs 23.2.1 (i686-pc-linux-gnu, GTK+ Version 2.24.4), running on Ubuntu 11.04. |
|||
| #412 | fixed | coq parsing broken since Jun 04 20:12:40 (II) | ||
| Description |
Here is another piece of Coq code that doesn't parse anymore: Record a : Type := make_a { aa : nat }.
|
|||
| #411 | wontfix | wiki formatting corrupts tickets | ||
| Description |
Please disable the wiki formatting for tickets. There are many tickets, where the formatting makes the contents unreadable or does even corrupt the contents. Bye, Hendrik |
|||
