formal position for PThm nodes;

proper context;

misc tuning and clarification, notably wrt. flow of context;

isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

tuned signature;

avoid Local_Theory.reset in application space

--HG--
extra : rebase_source : 085dbafb40406dfe49ff89a0341696228dcbd526

tuned signature;

tuned;

tuned proofs, to allow unfold_abs_def;

clarified signature;

eliminated "xname" and variants;

tuned signature;

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

tuned signature;

updated to infer_instantiate;

prefer tactics with explicit context;

{r,e,d,f}tac with proper context in BNF

tuned;

tuned;

tuned signature;

make SML/NJ more happy;

handle error messages also in after_qed

reorder some steps in the construction to support mutual datatypes

more readable error message if some types do not correspond to sort constraints of the datatype

better precomputing

equivalence in code_dt data structure must respect both rty and qty

don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned

go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used

Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype