more precise syntax antiquotations;

ML antiquotations for type classes;

read_class: perform actual read, with source position;

parallel brute-force disambiguation;

degrade gracefully in CRITICAL section;

gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;

tuned;

use simplified Syntax.escape;

tuned hyp_subst_tac';

use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes

merged

more work on the new monotonicity stuff in Nitpick

improved precision of infinite "shallow" datatypes in Nitpick; e.g. strings used for variable names, instead of an opaque type

cosmetics

merged

merged

adding no_topmost_reordering as new option to the code_pred command

adopting Mutabelle to quickcheck reporting; improving quickcheck reporting

added quiet option to quickcheck command

added basic reporting of test cases to quickcheck

merged

use abstract code cerficates for bare code theorems

implement quotient_of for odl SML code generator

adjusted to cs. e4a7947e02b8

bound argument for abstype proposition

renamed theory Rational to Rat

tuned whitespace

more precise exception handler

more general case and induct rules; normalize and quotient_of; abstract code generation

crossproduct coprimality lemmas