[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.
locale poset =
assumes "order<=base×base" and "refl(base,order)" and "antisym(order)" and "trans(order)"
locale strict_poset =
assumes "strict_order<=base×base" and "irrefl(base,strict_order)" and "antisym(strict_order)" and "trans(strict_order)"
locale strict = poset "base" "order - id(base)"
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and