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

tuned;

access X11 window manager;

new codatatype example: stream processors

use the right context in tactic

fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments

do not use wrong constructor in auto-generated proof goal

fixed de Bruijn bug in 'unfold_lets'

tuned error message

reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes

strengthened tactics w.r.t. 'lets' and tuples