equal
deleted
inserted
replaced
12 ind.ML a simple induction package 
12 ind.ML a simple induction package 
13 induct_method.ML proof by cases and induction on sets and types (Isar) 
13 induct_method.ML proof by cases and induction on sets and types (Isar) 
14 linorder.ML transitivity reasoner for linear (total) orders 
14 linorder.ML transitivity reasoner for linear (total) orders 
15 quantifier1.ML simplification procedures for "1 point rules" 
15 quantifier1.ML simplification procedures for "1 point rules" 
16 simp.ML powerful but slow simplifier 
16 simp.ML powerful but slow simplifier 
17 simplifier.ML fast simplifier 

18 split_paired_all.ML turn surjective pairing into split rule 
17 split_paired_all.ML turn surjective pairing into split rule 
19 splitter.ML performs case splits for simplifier.ML 
18 splitter.ML performs case splits for simplifier 
20 typedsimp.ML basic simplifier for explicitly typed logics 
19 typedsimp.ML basic simplifier for explicitly typed logics 
21 
20 
22 directory Arith: 
21 directory Arith: 
23 abel_cancel.ML cancel complementary terms in sums of Abelian groups 
22 abel_cancel.ML cancel complementary terms in sums of Abelian groups 
24 assoc_fold.ML fold numerals in nested products 
23 assoc_fold.ML fold numerals in nested products 