merged

tuned signature;

simplifier uses proper Proof.context instead of historic type simpset;

merged

avoided map_of in def of fun_rep (but still needed for efficient code)

spelling

spelling

tuned

complete revision: finally got rid of annoying L-predicate

moved leastness lemma

proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2); speculative update for yap (untested);

use automatic type coerctions in Sqrt example

make SML/NJ happy;

not all Nitpick 'constructors' are injective -- careful

added another definition snipped

actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;

modifiers for classical wrappers operate on Proof.context instead of claset;

removed historic comments;

tuned exceptions -- avoid composing error messages in low-level situations;

tuned signature; tuned comments;

proper identifiers -- avoid crash of case translations;

reduced duplication

do not add case translation syntax in rep_datatype compatibility mode

run type inference on input to wrap_data

installed case translations in BNF package

tuned

more antiquotations;

tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side; declare command "print_case_translations" where it is actually defined;