[isabelle] TERM exception in fologic.ML



Back in October 2014 I reported an error that I encountered when updating IsarMathLib to Isabelle 2014.The error is still there in Isabelle2016-RC1. This can be replicated by checking the following theory (in Isabelle/ZF logic): 
theory Scratch imports func

begin

lemma func_imagedef: assumes A1: "f:X\<rightarrow>Y" and A2: "A\<subseteq>X"
 shows "f``(A) = {f`(x). x \<in> A}"
proof
 from A1 show "f``(A) \<subseteq> {f`(x). x \<in> A}"
ÂÂÂ using image_iff apply_iff by auto
 show "{f`(x). x \<in> A} \<subseteq> f``(A)"
 proof
ÂÂÂ fix y assume "y \<in> {f`(x). x \<in> A}"
ÂÂÂ then obtain x where "x\<in>A \<and> y = f`(x)"
ÂÂÂÂÂ by auto
ÂÂÂ with A1 A2 show "y \<in> f``(A)"
ÂÂÂÂÂ using apply_iff image_iff by auto
 qed
qed

end
which givesÂ
exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
 dest_Trueprop
 âf A B.
ÂÂÂÂ âa b. f â Pi(A, B) â
ÂÂÂÂÂÂÂÂÂÂ âa, bâ â f â a â A â f ` a = b
in Isabelle/jEdit tooltip at the last auto keyword.
This is not a very important problem for me as I can work around it, but maybe it's good to know that it is still there.
Slawomir Kolodynski



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