[isabelle] How to make these cyclic locales to work?



Please explain why the below theory does not verify and how to make it to verify.

I need this knowledge in order to develop order/lattices theory for IsarMathLib.

theory test
  imports Main_ZF
begin

locale loc1 =
  fixes s::i
  assumes "0 ~: s"

locale loc2 =
  fixes s::i
  assumes "0 : s"

sublocale loc1 < loc2 "s Un {0}" sorry

sublocale loc2 < loc1 "s - {0}" sorry

interpretation inter: loc1 "0"
sorry

end

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





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