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

dropped axclass; dropped Id

dropped axclass; dropped Id; session theory Hoare.thy

dropped axclass

export prs_rules and rsp_rules attributes

merge

improved precision of small sets in Nitpick

improved Nitpick's support for quotient types

Forgot to check NSA in changeset e4a431b6d9b7 ; Removed import of Integration

catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example

mind the "s"

merged

NEWS

added missing separator

more accurate when registering new types

added Dlist

tuned text

distributed theory Algebras to theories Groups and Lattices

merged

proper distinction of code datatypes and abstypes

merged

merged

merged

lemma distinct_insert

proper header and subsection headings

remove unneeded premise from rat_floor_lemma and floor_Fract

Replaced Integration by Multivariate-Analysis/Real_Integration

Support for one-dimensional integration in Multivariate-Analysis

Equivalence between DERIV and one-dimensional derivation in Multivariate-Analysis

merged

add mixfix field to type Domain_Library.cons

remove unnecessary local

update to use fixrec package

merge

enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit

filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)

dropped references to old axclass from documentation

Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation contained variables bound by meta level quantifiers.

fixed a few bugs in Nitpick and removed unreferenced variables

update the keywords files

rename print_maps to print_quotmaps