Added tag Isabelle2013-1-RC1 for changeset c37100233af7

reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code

removed dead code

added check to avoid odd situations the N2M code cannot handle

reverted check introduced in ce58fb149ff6, now that independent functions are allowed (cf. 347c3b0cab44)

tuned signature

handle independent functions defined in parallel in N2M (in presence of type variables, see ce58fb149ff6)

tuned

tuned

qualifed popular user space names

dropped obsolete check: dest_num always yields positive number

simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number

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