Declare isKResult with sort information

isKResult was previously declared as a KLabel constant,
now it is declared as a function in Bool.

Ths test output changes because a bare KLabel and a function-style
production pretty-print with different whitespace.
The modified regular expression explicitly ignores whitespace
rather than hardcoding one or the other, so it works with both versions.
give "size" distinct labels on different sorts

This adds klabel addtributes so the "size" functions for
List/Map/Set get unique labels. As I see we did with
the member ship test "in", I let Set keep the default label.
Initial Coq backend.

This adds --backend option coq
which generates Coq files defining the sorts and rules of a definition.

This first generates a file containing a parsed version of the rules of
the definition, and then runs a separate "kcoq" binary which generated
the actual Coq files by reading rule bodies from the generated file and
reading syntax from the actual .k files. The kcoq binaries are not
included in this commit.
Copyright notices
Let wait for kcoq process be interrupted

The best a Backend's run method can do with InterruptedException
is to be sure to set the thread's interrupted status before it
returns.
This patch immediately gives up on compiling if it gets interrupted
while waiting for the child process to finish, and returns immediately
from the backend after killing the child process.
latex pretty-printing merged
Merge pull request #801 from bmmoore/coq-backend

Coq backend
Ids should not be preceded by numbers either.
Merge pull request #808 from kframework/fixIdRegex

Ids should not be preceded by numbers either.
Merge pull request #810 from grosu/kast-in-K

Kast in k
Merge branch 'kast-in-K' of https://github.com/grosu/k into kast-in-K
added some kast syntax: variables, configurations, basic terms
Merge branch 'kast-in-K' of https://github.com/grosu/k into kast-in-K