Rene Thiemann <rene.thiemann@uibk.ac.at> [Fri, 15 Apr 2016 10:19:35 +0200] rev 63027
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)
haftmann [Mon, 18 Apr 2016 20:56:18 +0200] rev 63026
fragment of a HOL type class primer
haftmann [Mon, 18 Apr 2016 20:56:13 +0200] rev 63025
capitalized GCD and LCM syntax
haftmann [Mon, 18 Apr 2016 20:56:11 +0200] rev 63024
environment variable check has become pointless after 771b8ad5c7fc
traytel [Tue, 19 Apr 2016 13:05:50 +0200] rev 63023
unfold internal definitions before emitting a proof obligation
wenzelm [Tue, 19 Apr 2016 12:06:34 +0200] rev 63022
more IDE support for Isabelle/Pure bootstrap;
wenzelm [Mon, 18 Apr 2016 22:51:32 +0200] rev 63021
merged
wenzelm [Mon, 18 Apr 2016 20:43:37 +0200] rev 63020
tuned signature;
wenzelm [Mon, 18 Apr 2016 20:24:19 +0200] rev 63019
prefer internal attribute source;
paulson <lp15@cam.ac.uk> [Mon, 18 Apr 2016 16:50:19 +0100] rev 63018
tidying some proofs; getting rid of "nonempty_witness"