1name: hol-sort-unint 2version: 1.0 3description: HOL sorting theories (before re-interpretation) 4author: HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> 5license: MIT 6main { 7 import: sorting 8 import: mergesort 9} 10sorting { 11 article: "sorting.ot.art" 12} 13mergesort { 14 import: sorting 15 article: "mergesort.ot.art" 16} 17