summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

merged

fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

more robust ML pretty printing (cf. b6c527c64789);

tuned;

renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library

tuned text

tuned names to avoid shadowing

merge Gcd/GCD and Lcm/LCM

clarify types of terms: use proper set type

instance bool :: linorder