Changes

Spock is an XO activity and pygtk application that implements a simple text editor with

Spock is an XO activity and pygtk application that implements a simple text editor with

an embedded proof verifier.  The proof verifier is based on the

an embedded proof verifier.  The proof verifier is based on (an older version of) the

[http://sites.google.com/a/ghilbert.org/ghilbert/home Ghilbert] proof language,

[http://sites.google.com/a/ghilbert.org/ghilbert/home Ghilbert] proof language,

with some modest extensions.  Ghilbert in turn is inspired by the

with some modest extensions.  Ghilbert in turn is inspired by the