make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules

move lemma dvd_mod_imp_dvd into class semiring_div

merged

improved treatment of case certificates

repaired order of variable node allocation

explicitly import Fact

change imports to move Fact.thy outside Plain

add lemmas poly_{div,mod}_minus_{left,right}

merged

declare scaleR distrib rules [algebra_simps]; cleaned up

clean up instantiations

merged

simplify some proofs

remove duplicate instance declaration

stripped classrels_of, instances_of

use canonical subalgebra projection

experimental switch to new well-sorting algorithm

handle NONE case in arity function properly

clarified status of variables in evaluation terms; tuned header

subalgebra: drop arities if desired

merged

more liberality needed

merged

added lemmas

merged

simplified evaluation

merged

added dvd_div_mult