Re: [isabelle] Underlined subgoals

Ok, I tracked one example down, it seems to be the case-expression

In the first lemma, everything from the line of the case-expression
onwards is underlined
lemma "(case x of 0 \<Rightarrow> True | Suc i \<Rightarrow> True)" oops

If the next lemma is shown in multiple lines in the subgoals-buffer,
only the line of the case-expression and subsequent lines appear underlined.
  underlined; (case x of 0 \<Rightarrow> True | Suc i \<Rightarrow>
True); also_underlined\<rbrakk> \<Longrightarrow> True"

It seems to be some syntactic matter, not depending on whether constants
are defined or not


Peter Lammich wrote:
> Makarius wrote:
>> On Sat, 29 Dec 2007, Peter Lammich wrote:
>>> in the new ProofGeneral shipped with the 2007 version, sometimes the 
>>> subgoals in the goals-buffer are underlined, sometimes only the 
>>> conclusion part of the subgoal.
>> Very strange.  Which version of Emacs is this?
> Emacs: [version 21.4.20; December 2006]
> ProofGeneral: Version 3.7pre071112.
> When I have a reproducible example, I'll also post it. Currently I have
> none, because I thought it was some feature, not a bug and did not
> isolate one.
> regards,
>         Peter

Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich at
Tel: 0251-83-32749
Mobil: 0163-5310380

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