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

use INF and SUP on conditionally complete lattices in multivariate analysis

add SUP and INF for conditionally complete lattices

use bdd_above and bdd_below for conditionally complete lattices

generalize SUP and INF to the syntactic type classes Sup and Inf

added some N2M caching

also generalize fixed types

generalize types when synthetizing n2m (co)recursors, to facilitate reuse

nicer error message in case of duplicates

use int example like in the rest of IMP (instead of nat)

dropped dead code

fact generalization and name consolidation

streamlined setup of linear arithmetic

make 'try0' return faster when invoked as part of 'try'

careful with lists of different lengths

split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')