A generic arithmetic prover based on Positivstellensatz certificates --- also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination
(* Title: HOL/Word/Word.thy
Author: Gerwin Klein, NICTA
*)
header {* Word Library interafce *}
theory Word
imports WordGenLib
begin
text {* see @{text "Examples/WordExamples.thy"} for examples *}
end