more antiquotations;

proper spec_rule name via naming/binding/Morphism.binding;

proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory";

tuned -- avoid confusion of fun_t with fun_lhs;

avoid shadowing of local bindings -- more maintainable;

more informative spec rules: optional name;
clarified signature;
more thorough treatment of Thm.trim_context vs. Thm.transfer;

formal position for PThm nodes;

more informative Spec_Rules.Equational, notably primrec argument types;

isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

proper concept of code declaration wrt. atomicity and Isar declarations

--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472

more uniform errors in '(prim)(co)rec(ursive)' variants

print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'

export ML functions (towards nonuniform codatatypes) + signature tuning

generalized ML function (towards nonuniform datatypes)

only recognize maps if the type names match

robustness

extended ML signature + refactored

tuning

tuned signature;

clarified syntax;

explicit tagging of code equations de-baroquifies interface

--HG--
extra : rebase_source : 1d83d31f669dc30b586df508a64fdc3a9e7b2655

made parsing of monomorphic/polymorphic constants more robust

more flexible parsing (towards type class support)

allow 'for' fixes for multi_specs;

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

prefer binding over base name;

Type_Infer.object_logic controls improvement of type inference result;

tuning

more natural order for 'cong_intros'

renamed generated theorem

avoid 'prove_sorry' for unreliable tactics

reused code

tuning

more reliable check for rhs variables

sorted out type issue with sort constraints

moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle