New features: permissive option for fixrec to skip proofs of equations; side conditions for fixrec equations (for definedness); fixpat theorem names apply to entire group of theorems; improved error messages

added match functions for spair, sinl, sinr

fixed \<Prod> syntax

new

Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers. Will now signal if ATP has run out of time and then kill the watcher.

* Pure: the Isar proof context type is already defined early in Pure as Context.proof;