Theory EPAC_Checker_Init

(*
  File:         PAC_Checker_Init.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory EPAC_Checker_Init
  imports EPAC_Checker PAC_Checker.WB_Sort PAC_Checker.PAC_Checker_Relation
begin

section ‹Initial Normalisation of Polynomials›

subsection ‹Sorting›

text ‹Adapted from the theory \<^text>‹HOL-ex.MergeSort› by Tobias Nipkow. We did not change much, but
   we refine it to executable code and try to improve efficiency.
›

end