equal
deleted
inserted
replaced
16 split_paired_all.ML turn surjective pairing into split rule 
16 split_paired_all.ML turn surjective pairing into split rule 
17 splitter.ML performs case splits for simplifier.ML 
17 splitter.ML performs case splits for simplifier.ML 
18 typedsimp.ML basic simplifier for explicitly typed logics 
18 typedsimp.ML basic simplifier for explicitly typed logics 
19 
19 
20 directory Arith: 
20 directory Arith: 

21 abel_cancel.ML cancel complementary terms in sums of Abelian groups 

22 assoc_fold.ML fold numerals in nested products 

23 cancel_numerals.ML cancel common coefficients in balanced expressions 
21 cancel_factor.ML cancel common constant factor 
24 cancel_factor.ML cancel common constant factor 
22 cancel_sums.ML cancel common summands 
25 cancel_sums.ML cancel common summands 
23 nat_transitive.ML simple package for inequalities over nat 
26 combine_numerals.ML combine coefficients in expressions 

27 fast_lin_arith.ML generic linear arithmetic package 