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.


	Makarius






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