adapted to authentic syntax -- actual types are verbatim;

authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;

more systematic mark/unmark operations; tuned;

proper (type_)notation;

proper antiquotations;

standard convention for syntax consts;

more precise scope of exception handler;

eliminated hard tabs;

tuned final whitespace;

repaired 'definition' (cf. d8d7d1b785af);

merged

more recdef (and old primrec) hunting

killed recdefs in HOL-Auth

merged

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

export add_quotient_type.

updated generated files;

added type_notation command;

more uniform treatment of syntax for types vs. consts;

made smlnj happy

more antiquotations;

more antiquotations; eliminated legacy ML bindings;

modernized structure Term_Ord;

use existing Typ_Graph;

further standard instances of functor Graph;

code simplification by inlining;

just one copy of structure Term_Graph (in Pure);

modernized structure Int_Graph;

clarified @{const_name} vs. @{const_abbrev};

clarified @{const_name} (only logical consts) vs. @{const_abbrev}; tuned;

type/const name: explicitly allow abbreviations as well;

clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;

added at-poly-test, which is intended for performance tests of Poly/ML itself;

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