Summary
- several updates on polynomial long division and pseudo division - division of polynomials is now available on idom_divide (was field before) - added polynomial pseudo division (on comm_ring_1) - improved code equation for polynomial (pseudo)-division (joint work of S. Joosten, R. Thiemann, and A. Yamada)
- fragment of a HOL type class primer
- capitalized GCD and LCM syntax
- environment variable check has become pointless after 771b8ad5c7fc
The file was modified | src/HOL/Library/Polynomial.thy (diff) |
The file was added | src/Doc/Typeclass_Hierarchy/Setup.thy |
The file was added | src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy |
The file was added | src/Doc/Typeclass_Hierarchy/document/build |
The file was added | src/Doc/Typeclass_Hierarchy/document/root.tex |
The file was added | src/Doc/Typeclass_Hierarchy/document/style.sty |
The file was modified | src/Doc/ROOT (diff) |
The file was modified | src/Doc/manual.bib (diff) |
The file was modified | src/Doc/more_antiquote.ML (diff) |
The file was modified | src/HOL/GCD.thy (diff) |
The file was modified | src/Tools/Code/code_ml.ML (diff) |
The file was modified | src/Tools/Code/code_target.ML (diff) |