formal position for PThm nodes;

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

isabelle update -u control_cartouches;

tuned signature -- eliminated clones;

make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions

tuned signature;

tuned proofs, to allow unfold_abs_def;

clarified signature;

less resetting of local theories

tuned signature;

making 'pred_inject' a first-class BNF citizen

refactoring

derive transfer rule for predicator

make predicator a first-class bnf citizen

reverted inadvertently qfinished/pushed change r164eeb2ab675

set "transfer_rule" attribute more generously

disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier

tuned signature;

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

more graceful failure if some of the involved BNFs have no data

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned signature -- prefer qualified names;

eliminated some clones of Proof_Context.cterm_of

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

tuning

tuned; store pred_simps

added pred_def, rel_eq_onp tuned

allow sorts on dead variables in BNFs

proper context for assume_tac (atac remains as fall-back without context);

made SML/NJ happy;

register transfer rules from BNF and FP_Sugar

refactored

Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;

refactor fp_sugar move theorems

added missing 'restore' in 'transfer' plugin

honour sorts in N2M

made code work also in the presence of deads

use right sort constraints

pretend code generation is a ctr_sugar plugin

named interpretations

tuned size function generation

introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales

use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)

compile

predicator simplification rules: support also partially specialized types e.g. 'a * nat

localize new size function generation code

manual merge + added 'rel_distincts' field to record for symmetry

observe also DEADID BNFs and associate the conjunction in rel_inject to the right

setup for Transfer and Lifting from BNF; tuned thm names

--HG--
rename : src/HOL/Tools/transfer.ML => src/HOL/Tools/Transfer/transfer.ML