work around bug in CVC4, with boolean arguments to (co)datatypes

other way of crashing (with CVC4)

set right logic for CVC4 with (co)datatypes

removed explicit '--quant-cf' option to CVC4, now that it's the default

more accurate lemma name

parse CVC4 unsat cores

tuning

removed redundant code line

clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;

add reindex rules for distr and nn_integral on count_space

generalized lemmas and tuned proofs

generalized lemmas (particularly concerning dvd) as far as appropriate

formally self-contained gcd type classes

merged

no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";

use \isastyletext directly via 'text' command;

proper sequential version (cf. 302104d8366b);

documentation stubs about permanent_interpretation

cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory

merged

import general theorems from AFP/Markov_Models

uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;

tuning

merged

do not introduce consts too early unnecessarily

added lemma

merged

prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;

make SML/NJ happy;

more careful ML source positions, for improved PIDE markup;

NEWS

tuned proofs

added quickcheck[approximation]

quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}

disjunction and conjunction for forms

truncate intermediate results in horner to improve performance of approximate; more efficient truncated addition float_plus_up/float_plus_down

added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction

cancel real of power of numeral also for equality and strict inequality; simplify floor of power of numeral; lemmas about real/floor

simplified computations based on round_up by reducing to round_down; more general round_up_le1, round_up_less1, round_down_ge1, round_up_le0

code equation for powr

merged

more careful ML source positions, for improved PIDE markup;

more position information, e.g. relevant for errors in generated ML source;

more symbols;

tuned whitespace;

more markup;

simplifie sessions;

more Isar proof methods;

more Isar proof methods;

more Isar proof methods;

add forgotten lemma

added lemma

make 'corec_transfer' tactic more robust

also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables

make 'rec_transfer' tactic more robust

add del option to measurable; make measurability rules available as dynamic theorem;

merged

proper context for assume_tac (atac remains as fall-back without context);

even -> evn because even is now in Main

dropped redundant transfer rules (now proved and registered by datatype and plugins)