[isabelle] Problems with coercions



Dear All,

consider the following theory

theory Test
  imports HOL.Complex 
begin

lemma "{x. cmod x = sr} = range (op * sr)"
proof -
  show "{x. cmod x = sr} = range (op * sr)"
  (* failed to refine any pending goal *)
  text âproof line is parsed as @{term "{x. cmod (complex_of_real x) = sr} = range (op * sr)"}â 
  text âgoal is parsed as       @{term "{x. cmod x = sr} = range (op * (complex_of_real sr))"}â
  oops

end


Here, the same formula is parsed differently in the lemma-statement and in the proof,
which at least I found quite confusing.

The effect appears in both Isabelle 2017-RC3 as well as in c90fb8bee1dd.

Cheers,
RenÃ


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