Tue, 10 Nov 2015 14:43:29 +0000 Merge
paulson <lp15@cam.ac.uk> [Tue, 10 Nov 2015 14:43:29 +0000] rev 61610
Merge
Tue, 10 Nov 2015 14:18:41 +0000 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk> [Tue, 10 Nov 2015 14:18:41 +0000] rev 61609
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Tue, 10 Nov 2015 14:46:11 +0100 subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm [Tue, 10 Nov 2015 14:46:11 +0100] rev 61608
subdegree/shift/cutoff and Euclidean ring instance for formal power series
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip