Expressed most Oops rules using Notes instead of Says, and other tidying

added split_paired_Ex to the implicit simpset

added select_equality to the implicit claset

added select_equality to the implicit claset added split_paired_Ex, split_part, and Eps_split_eq to the implicit simpset removed split_select renamed Collect_Prod to Collect_split

added newline at end of file

*** empty log message ***

streamlined specification of included theories

corrected Title

removed obsolete comment

added Univalent

removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses

added update_same, update_other, update_triv, and map_of_SomeD

replaced fn _ => by K

*** empty log message ***

New rule: image_subset

Restored the ciphertext in OR4 in order to make the spec closer to that in OtwayRees.thy

Tidied by adding more default simprules

adapted to new split order;

adapted to new sort function;

improved targets; fixed dependencies on parent logics;

tuned;

added -u option (again);

Now calls Blast_tac more often

obsolete;

feeder;

Changed required by new blast_tac (the one that squashes flex-flex pairs)

Blast_tac now squashes flex-flex pairs immediately

New theorem image_subsetI

Making proofs faster, especially using keysFor_parts_insert

do require perl;