Источник / закреплённая редакция
isabelle.order
Источник пакета isabelle.order · sha256:e5988d63317612732ff10702b24bea8bd749a8c62b04f51db1eb338f36f5a17e
- work
- urn:arxo:isabelle.order#Import_Source_554244b7236710a2597dff85acd1947c517fc88f2e1aeae905b370af20a0c6b3
- номер
- sha256:e5988d63317612732ff10702b24bea8bd749a8c62b04f51db1eb338f36f5a17e
- вид
- urn:arxo:isabelle.order#treatise
Import_Edition_554244b7236710a2597dff85acd1947c517fc88f2e1aeae905b370af20a0c6b3
- edition
- urn:arxo:isabelle.order#Import_Edition_554244b7236710a2597dff85acd1947c517fc88f2e1aeae905b370af20a0c6b3
- язык
- en
- официальность
- official
- материализация
- PINNED_OFFICIAL_BYTES
- жизненный цикл
- —
Публикации
| URI | Тип | documentHash | Получено |
|---|---|---|---|
| https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2025-2/src/HOL/Orderings.thy | text/plain; charset=utf-8 | sha256:9504399a7e06d858a65fb2c0e2613ffe33d1b179fe7a203eb5b4d90b9fd10406 | 2026-09-07T23:38:59Z |
Фрагменты — 3
Orderings.preorder_class.le_less_trans · lemma · на него ссылаются: 1
en · official · sha256:05f9d1dac5f4816e5a501bc9604cb56945dcd93d7904798cf02297e30c07cd9bEN
lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"Ссылаются нормы: Import_Rule_2bbcae2cd2f015a5e79d256e59269689eaf32b8a5d2cff20c1e8029f9dbec088
Orderings.preorder_class.less_trans · lemma · на него ссылаются: 1
en · official · sha256:c575b3df4023c1762888a1016adcba7864c3030a8431f3c6ff7ba6192e1e2cf6EN
lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"Ссылаются нормы: Import_Rule_ba9f606b3dfff6f0efb044b968493c82752c7719f3ec01a66d852f23de4aa087
Orderings.preorder_class.less_imp_le · lemma · на него ссылаются: 1
en · official · sha256:657cb837a2b70cc29e02141be0685085b8bb50399ae3bd526da44bc3e648bf21EN
lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"Ссылаются нормы: Import_Rule_d7f7657f6e55615a91c9c02daa264114e1e11bbf2b338953074bacd124f339ca
Хэш рядом с текстом — sha256 его точных байтов. Он и есть проверка того, что показанный текст совпадает с закреплённым в пакете: расхождение роняет статику оракула.