Re: [isabelle] Isabelle2008: Strange behavior with sets and intro!: ext or intro!: le_funI
On Mon, 9 Jun 2008, Peter Lammich wrote:
> Given a lemma:
> lemma fixes S:: "'a \<Rightarrow> 'b set" and S' shows "S'\<le>S"
> I do
> apply (clarify intro!: le_funI)
> and would expect (as in Isabelle2007):
> !!x xa. xa : S' x ==> xa : S x
> instead, I get the subgoal:
> !!x xa. S' x xa ==> S x xa
> In Isabelle 2007, this would not even typecheck, but Isabelle2008 seems to
> accept it valid (I think, using the characteristic function of the set).
This is due to a fundamental change in HOL, see the NEWS where it says
``Turned the type of sets "'a set" into an abbreviation for "'a =>
bool"''; there are also some hints how to convert existing theories.
This archive was generated by a fusion of
Pipermail (Mailman edition) and