adding an example with integers and String.literals

adding an example to show how code_pred must be invoked with locales

removing report from the arguments of the quickcheck functions and refering to it by picking it from the context

changing the container for the quickcheck options to a generic data

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons

changing String.literal to a type instead of a datatype

increasing the number of iterations to ensure to find a counterexample by random generation

only conceal primitive definition theorems, not predicate names