Sorting-in-HOL4

To port chapter 2 - sorting from the book "Functional Data Structures and Algorithms" to HOL4

Provide feedback

Name		Name	Last commit message	Last commit date
Latest commit History 8 Commits
.HOLMK		.HOLMK
.hollogs		.hollogs
.holobjs		.holobjs
README.md		README.md
bottomup_mergesortCorrectnessScript.sml		bottomup_mergesortCorrectnessScript.sml
bottomup_mergesortCorrectnessTheory.sig		bottomup_mergesortCorrectnessTheory.sig
insertionsortCorrectnessScript.sml		insertionsortCorrectnessScript.sml
insertionsortCorrectnessTheory.sig		insertionsortCorrectnessTheory.sig
natural_mergesortCorrectnessScript.sml		natural_mergesortCorrectnessScript.sml
natural_mergesortCorrectnessTheory.sig		natural_mergesortCorrectnessTheory.sig
quicksortCorrectnessScript.sml		quicksortCorrectnessScript.sml
quicksortCorrectnessTheory.sig		quicksortCorrectnessTheory.sig
topdown_mergesortCorrectnessScript.sml		topdown_mergesortCorrectnessScript.sml
topdown_mergesortCorrectnessTheory.sig		topdown_mergesortCorrectnessTheory.sig