2013-11-10 haftmann 2013-11-10 simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number
2013-11-08 nipkow 2013-11-08 more exercises
2013-11-08 blanchet 2013-11-08 by (auto ...)[1] not by (auto [1])
2013-11-08 nipkow 2013-11-08 added exercise
2013-11-07 kleing 2013-11-07 Add output translation for <a := .., b := .., ..> state notation.
2013-11-07 blanchet 2013-11-07 reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables)
2013-11-07 blanchet 2013-11-07 more docs
2013-11-07 blanchet 2013-11-07 properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
2013-11-06 blanchet 2013-11-06 reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP
2013-11-06 blanchet 2013-11-06 simplified code
2013-11-06 blanchet 2013-11-06 fourth attempt at generalizing N2M types (to leverage caching)
2013-11-06 blanchet 2013-11-06 tuning
2013-11-05 hoelzl 2013-11-05 int and nat are conditionally_complete_lattices
2013-11-06 blanchet 2013-11-06 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'
2013-11-06 blanchet 2013-11-06 removed dead code
2013-11-06 blanchet 2013-11-06 update docs
2013-11-06 blanchet 2013-11-06 take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case
2013-11-06 blanchet 2013-11-06 took out loopy code
2013-11-06 blanchet 2013-11-06 take out even less aggressive generalization -- it's still too aggressive
2013-11-06 blanchet 2013-11-06 reverted too aggressive 7cb8442298f0
2013-11-06 blanchet 2013-11-06 generalize more aggressively
2013-11-05 blanchet 2013-11-05 avoid subtle failure in the presence of top sort
2013-11-05 blanchet 2013-11-05 tuning
2013-11-05 blanchet 2013-11-05 get mutually recursive maps as well
2013-11-05 hoelzl 2013-11-05 tuned proofs in Approximation
2013-11-05 blanchet 2013-11-05 fixed subtle name shadowing bug
2013-11-05 blanchet 2013-11-05 use right permutation in 'map2'
2013-11-05 blanchet 2013-11-05 stronger normalization, to increase n2m cache effectiveness
2013-11-05 blanchet 2013-11-05 make local theory operations non-pervasive (makes more intuitive sense)
2013-11-05 hoelzl 2013-11-05 NEWS
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-05 hoelzl 2013-11-05 generalize bdd_above/below_uminus to ordered_ab_group_add
2013-11-05 hoelzl 2013-11-05 restrict Limsup and Liminf to complete lattices
2013-11-05 hoelzl 2013-11-05 use INF and SUP on conditionally complete lattices in multivariate analysis
2013-11-05 hoelzl 2013-11-05 add SUP and INF for conditionally complete lattices
2013-11-05 hoelzl 2013-11-05 use bdd_above and bdd_below for conditionally complete lattices
2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
2013-11-05 blanchet 2013-11-05 added some N2M caching
2013-11-05 blanchet 2013-11-05 also generalize fixed types
2013-11-05 blanchet 2013-11-05 generalize types when synthetizing n2m (co)recursors, to facilitate reuse
2013-11-05 blanchet 2013-11-05 nicer error message in case of duplicates
2013-11-05 kleing 2013-11-05 use int example like in the rest of IMP (instead of nat)
2013-11-04 haftmann 2013-11-04 dropped dead code
2013-11-04 haftmann 2013-11-04 fact generalization and name consolidation
2013-11-04 haftmann 2013-11-04 streamlined setup of linear arithmetic
2013-11-04 blanchet 2013-11-04 make 'try0' return faster when invoked as part of 'try'
2013-11-04 blanchet 2013-11-04 careful with lists of different lengths
2013-11-04 blanchet 2013-11-04 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
2013-11-04 blanchet 2013-11-04 better error handling
2013-11-04 traytel 2013-11-04 more robust treatment of dead variables in n2m
2013-11-04 blanchet 2013-11-04 more robust n2m w.r.t. 'let's
2013-11-04 blanchet 2013-11-04 tuning
2013-11-04 blanchet 2013-11-04 strengthened tactic
2013-11-04 blanchet 2013-11-04 made n2m code more robust w.r.t. advanced constructs (e.g. lambdas)
2013-11-04 blanchet 2013-11-04 handle constructor syntax in n2m primcorec
2013-11-04 blanchet 2013-11-04 typo
2013-11-04 blanchet 2013-11-04 made sugared 'coinduct' theorem construction n2m-proof
2013-11-04 blanchet 2013-11-04 moved code around
2013-11-04 blanchet 2013-11-04 tuning
2013-11-04 blanchet 2013-11-04 make code more robust w.r.t. applied/unapplied map (primrec vs. primcorec)