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.
lemma
"\<lbrakk>not_underlined;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;
  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

regards,
  Peter

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 uni-muenster.de
Tel: 0251-83-32749
Mobil: 0163-5310380






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