Custom Query (361 matches)

The options "Search Rewrite ..." and "Search About ..." do not work in the pre-release (ProofGeneral-3.7pre070312)

To fix the problem I had to patch the file coq.el. I include the corrected version.

In coq, when doing large proofs, the goals window tends to not be centered on the right information: it only shows the oldest assumptions, and when the list of assumption is too long, it does not even show the statement of the first goal.

I suggest centering on bar of equal signs that separates the most recent hypotheses from the current goal. I did it by modifying two files: proof-utils.el and pg-goals.el

While I think that the modification on proof-utils.el can be shared with other proof systems (I only add the possibility that the target point could be given by a string that will be searched in the buffer), the change done on pg-goals.el is coq-specific and should not be left there, but I could not find how to make the code customizable in this respect.

So this is a suggestion for modification, but this should be reviewed to make it more generic in its approach.

Any idea how I can get rid of the characters such as Ú that appear in the Isabelle shell buffer? XEmacs doesn't display them, but they appear if printed or pasted into other text files.

+++    ~(c_BT_Obt_OLf t_a = c_BT_Obt_OLf t_a)Û
Ú+++ INFERENCE: Equality
+++ {lit = ~(c_BT_Obt_OLf t_a = c_BT_Oreflect t_a (c_BT_Obt_OLf t_a)),
+++  path = [1], res = c_BT_Obt_OLf t_a, lr = true, thm = |- F}Û
Ú+++   isa th: "False"  [.]Û
Ú+++ fol_term_to_hol: c_BT_Obt_OLf t_a = c_BT_Oreflect t_a (c_BT_Obt_OLf t_a)Û
Ú+++   result type: boolÛ
Ú