jm3.1
diophren
rmxdioph
pull out some parts of jm3.1 which will need to be reused in expdioph
expdioph !! !!
removal of trivial mathboxes
removal of anass1rs and others from a dozen proofs
minimal-change update to 13-Oct-14 set.mm
mathbox removal 2
switch permanently to set_clean.mm.  temporary copy of used mathbox statements
mathbox removal 3
cut loose FRSD for not pulling its weight
calling mathbox cleanup done.  can revisit
direct and amazingly short proof of fiphp3d that avoids Choice
redo the renclddom stuff to completely eliminate Choice from expdioph
not sure what, if anything I am going to do with this reproved fphpd/fphp combo
merge into work.mm and run the rewrapper
use the fphpdALT after all.  remove some antecedents
use the new infmrgelb.  tighter integration still TODO
reorganization of Stuff.  move back to keeping the mathbox in a separate file.  first commit of a bunch of stuff from last week