[isabelle] Feature suggestion: locales inside locales



The following does not verify. Accepting things like below would be useful. Please take this feature suggestion for Isabelle.

theory MyOrder
  imports Main_ZF
begin

locale poset =
  fixes base::i
  fixes order::i
  assumes "order<=base×base" and "refl(base,order)" and "antisym(order)" and "trans(order)"

locale strict_poset =
  fixes base::i
  fixes strict_order::i
  assumes "strict_order<=base×base" and "irrefl(base,strict_order)" and "antisym(strict_order)" and "trans(strict_order)"

context poset
begin
locale strict = poset "base" "order - id(base)"
end

end

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





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