[isabelle] Instatiating locales: where is the error?



theory test
  imports Main_ZF
begin

locale t =
  fixes "x"
  assumes "x=0"
begin
end

locale q = t "1"

end

How the locale q is instantiated without proof that "x=0" (in fact x is non-zero but instead "x=1"). I understand something about locales wrongly. Where is the error? How to obtain an instance of a locale?

-- 
Victor Porton - http://portonvictor.org





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