repaired definition (cf. d8d7d1b785af)

authentic syntax for *all* logical entities;

mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;

notation for xsymbols (cf. ad039d29e01c);

"_type_prop" is syntax const -- recovered printing of OFCLASS;

removed unused external_names;

cleanup type translations;

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

more precise exception handler

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

crossproduct coprimality lemmas

lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult

evaluation for abstypes

modernized structure Split_Rule; tuned signature; more antiquotations;

more antiquotations;

explicit @{type_syntax} markup;

explicit @{type_syntax} markup; misc tuning and simplification;

more orthogonal antiquotations for type constructors;

clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;

provide direct access to the different kinds of type declarations;

use mixfix syntax for Boogie types

merged

added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals

modernized syntax declarations, and make them actually work with authentic syntax;

observe standard convention for syntax consts;

proper type syntax (cf. 7425aece4ee3);

observe standard convention for syntax consts;

allow general mixfix syntax for type constructors;

merged

merged

remove redundant lemma realpow_increasing

remove redundant simp rules from RealPow.thy

adapt to new realpow rules

adapt to changes in simpset

moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power

move float syntax from RealPow to Rational

compile

merged

compile

make example compile

got rid of "axclass", apparently

merged

cosmetics

support local definitions in Nitpick

show Kodkod warning message even in non-verbose mode

distinguish between Kodkodi warnings and errors in Nitpick; will be needed starting with version 1.2.9 of Kodkodi

optimized multisets in Nitpick by fishing "finite"

document Quickcheck's "no_assms" option

tuned comment

merged

Moved old Integration to examples.

merged

merged

adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session

adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening

separated narrowing timeouts for intermediate and final steps

merged

merged

dropped axclass; dropped Id; session theory Hoare.thy

dropped session W0; c.f. MiniML in AFP

dropped axclass, going back to purely syntactic type classes