Re: [isabelle] Lost indexname in instantiated theorem: Eisbach messes up "of" and "where" attributes, when instantiating with "TYPE(...)"



> Consider the following theory, where I use the of and where attributes
> to instantiate a variable to "TYPE(nat)".
> Without Eisbach included, everything is fine. With Eisbach included, I
> get the error "Lost indexname in instantiated theorem".
> 
> What is going on here, and is there a workaround?

A possible workaround (except from not using Eisbach) is to use 
"Pure.of"/"Pure.where" instead of "of"/"where".

--
  Peter


> 
> --
>   Peter
> 
> 
> theory Scratch
> imports Main 
>   "~~/src/HOL/Eisbach/Eisbach"  (* Remove this line, and everything
> works fine *)
> begin
> 
>   consts f :: "'a â bool"
>   lemma foo: "f a â True" by auto
> 
>   thm foo[of "TYPE(nat)"]          (* Error: Lost indexname in
> instantiated theorem *)
>   thm foo[where a = "TYPE(nat)"]   (* Error: Lost indexname in
> instantiated theorem *)
> 
> end
> 
> 
> 






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