merged

slightly changing the enumeration scheme

adding some more test invocations of find_unused_assms

adding an example where random beats exhaustive testing

removing unnecessary assumptions in RComplete; simplifying proof in Probability

removing unnecessary assumptions in RealDef; simplifying proofs in Float, MIR, and Ferrack

one general list_all2_update_cong instead of two special ones

tuned comments;

standard Graph instances;

clarified signature -- avoid oddities of Iterable like Iterator.map; specific toString;

discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

explicit is better than implicit

dropped dead code

prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty; discontinued map_nodes, del_nodes conveniences -- avoid inefficient mapValues wrapper (this is not Table.map from ML); tuned signature;

tuned imports;

tuned signature;

discontinued obsolete Graph.all_paths (last seen in 1524d69783d3 and AFP/80bbbdbfec62);

merged

remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min

avoid using Int.succ_def in proofs

avoid using Int.succ or Int.pred in proofs

avoid using BIT_simps in proofs; rephrase lemmas without Int.succ or Int.pred;

avoid using BIT_simps in proofs

updated stats according to src/HOL/IsaMakefile;

more precise clean target;

clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;

avoid using Int.Pls_def in proofs

remove ill-formed lemmas word_pred_0_Min and word_m1_Min

remove ill-formed lemma of_bl_no; adapt proofs