more accurate context;

reactivate Thm.check_hyps, after adapting AFP/Datatype_Order_Generator (see AFP/b7e389b5765c);

check_hyps for attribute application (still inactive, due to non-compliant tools); bypass check_hyps for locale expressions, where assumptions are not necessarily declared in intermediate situations;

clarified context;

clarified context;

tuned signature;

shot in the dark to make LaTeX happy again

provide default name in splitted representation

dropped legacy alias feature

merged

disable Thm.check_hyps for now, due to remaining problems with AFP/Datatype_Order_Generator and AFP/Psi_Calculi (because of HOL-Nominal 'equivariance');

more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;

more accurate context;

tuned;

explicit check of background theory;

basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)

correctly extract code RHS, with loose bound variables

cope gracefully with missing ctr equations by plugging in 'False ==> ...'

strengthened tactic to handle 'disc_iff' equations of the form '... = False'

repair 'exhaustive' feature for one-constructor types

pass right rhs as code rhs

use correct default for exclude rules to avoid weird tactic failures

tuning (no need for |-> here)

fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')

tuning

only destruct cases equipped with the right stuff (in particular, 'sel_split')

generate 'disc_iff' for all discriminators

use 'disc_iff' as simp rules whenever possible + clean up '= True', '= False', etc.

exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial

merged

more robust;

merged