Insert Refinements and changes to QueryStructure to support them.
Added Query and Insert definitions so notations won't get
simplified by default.
Partial work on Min+Max

After much time failing to convince myself to work on this, I've
finally managed to get back to work.  I got mired in Ben's notations,
but, hopefully, he can help me out of my mire.

The idea is the following:

Say we have an ADT A and we want to delegate to an ADT B.  Then we
first refine to repA * repB, where we call both mutators in the
mutators, and ignore B in the observers.  This is the part that I'm
nearly done with.

Then we say that, given any relation R between repA and repB, if all
mutators respect R, then you can refine one observer at a time under
the assumption that that relation holds.  Here is were we'll want
tactic support for rewriting one pick into another pick, and then pick
into call, or something like that.

Finally, we say that if you provide a set of observers implemented
over the [snd] projection, and you provide two sets of mutators, one
of which uses only the [fst] and the other of which uses only the
[snd], then we can erase the [fst] projection.

Post-finally, we turn this into the min+max example.
Allow queries to return unordered results

The current query specification imposes a specific ordering for values
returned by observers; this commit introduces the "indistinguishable"
predicate (which asserts that two result sets are permutations of each
other), and relaxes the equality condition to indistinguishability: that
is, it requires that observers produce a result indistinguishable from
the reference output, instead of equal to it.
Merge branch 'master' of file://///afs/csail.mit.edu/group/plv/git/adt-synthesis
Create a process scheduler example, refined using a list-based implementation

(losely inspired by the example in Hawkins' "Data representation
synthesis" paper)

The list-based refinement is almost complete, though the implementation
doesn't yet satisfy the uniqueness constraints imposed by the schema.
Another, more interesting data structure using binary search trees is
sketched below.
Started constraint-free query structure modifications.
Merge branch 'master' of file://///afs/csail.mit.edu/group/plv/git/adt-synthesis
Partial work on min+max
Merge branch 'master' of file://///afs/csail.mit.edu/group/plv/git/adt-synthesis
Fixin' method lookup.
Fully working minimally super dependent lookup function.
Nice reasoning principle for default-free lookup.
Fully functional bounded lookup.
Need to move some code from String Bound to ilist.
Cleaned up / documented indexed list.
Finished switch back to ensembles.
Fixed small typo in honing tactics.
Finally got constraint enumeration working.
Cleaned up Insert refinements to satisfactory levels.
Work in progress: Implement a few ensemble-based refinements for the process scheduler example.