more exercises

by (auto ...)[1] not by (auto [1])

added exercise

Add output translation for <a := .., b := .., ..> state notation.

reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables)

more docs

properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel

reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP

simplified code

fourth attempt at generalizing N2M types (to leverage caching)

tuning

int and nat are conditionally_complete_lattices

be more open-minded and allow needless mutual recursion for 'prim(co)rec', since we allow it for '(co)datatype' -- eventual warnings (or errors) should be centralized in 'fp_bnf'

removed dead code

update docs

take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case

took out loopy code

take out even less aggressive generalization -- it's still too aggressive

reverted too aggressive 7cb8442298f0

generalize more aggressively

avoid subtle failure in the presence of top sort

tuning

get mutually recursive maps as well

tuned proofs in Approximation

fixed subtle name shadowing bug

use right permutation in 'map2'

stronger normalization, to increase n2m cache effectiveness

make local theory operations non-pervasive (makes more intuitive sense)

NEWS

move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)

generalize bdd_above/below_uminus to ordered_ab_group_add

restrict Limsup and Liminf to complete lattices