Source / pinned edition
isabelle.order
Source of package isabelle.order · sha256:e5988d63317612732ff10702b24bea8bd749a8c62b04f51db1eb338f36f5a17e
- work
- urn:arxo:isabelle.order#Import_Source_554244b7236710a2597dff85acd1947c517fc88f2e1aeae905b370af20a0c6b3
- number
- sha256:e5988d63317612732ff10702b24bea8bd749a8c62b04f51db1eb338f36f5a17e
- kind
- urn:arxo:isabelle.order#treatise
Import_Edition_554244b7236710a2597dff85acd1947c517fc88f2e1aeae905b370af20a0c6b3
- edition
- urn:arxo:isabelle.order#Import_Edition_554244b7236710a2597dff85acd1947c517fc88f2e1aeae905b370af20a0c6b3
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- —
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| 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 |
Fragments — 3
Orderings.preorder_class.le_less_trans · lemma · referenced by: 1
en · official · sha256:05f9d1dac5f4816e5a501bc9604cb56945dcd93d7904798cf02297e30c07cd9b
lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"Referencing norms: Import_Rule_2bbcae2cd2f015a5e79d256e59269689eaf32b8a5d2cff20c1e8029f9dbec088
Orderings.preorder_class.less_trans · lemma · referenced by: 1
en · official · sha256:c575b3df4023c1762888a1016adcba7864c3030a8431f3c6ff7ba6192e1e2cf6
lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"Referencing norms: Import_Rule_ba9f606b3dfff6f0efb044b968493c82752c7719f3ec01a66d852f23de4aa087
Orderings.preorder_class.less_imp_le · lemma · referenced by: 1
en · official · sha256:657cb837a2b70cc29e02141be0685085b8bb50399ae3bd526da44bc3e648bf21
lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"Referencing norms: Import_Rule_d7f7657f6e55615a91c9c02daa264114e1e11bbf2b338953074bacd124f339ca
The hash beside the text is the sha256 of its exact bytes. It is the check that the text shown matches the one pinned in the package: a divergence fails the oracle’s static analysis.