Examples call gocls to make goal clauses

Now labels the Horn and goal clauses to make the proof objects more readable

For the new version of name_thm. Now the same theorem is stored as is returned, as both contain a label and a link to the previous derivation. So get_thm no longer needs to attach a label to its resulting theorem.

name_thm no longer takes a theory argument, as the name no longer hides the previous derivation. Deleted sign_of_thm as redundant.

Printing & string functions moved to display.ML

Now loads deriv.ML