1name: hol-sort 2version: 1.0 3description: HOL sorting theories 4author: HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> 5license: MIT 6requires: base 7requires: hol-base 8show: "HOL4" 9show: "Data.Bool" 10show: "Data.List" 11show: "Data.Pair" 12show: "Function" 13show: "Number.Natural" 14show: "Relation" 15main { 16 article: "hol4-sort-unint.art" 17 interpretation: "../opentheory/hol4.int" 18} 19