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

strengthen tac w.r.t. lets with tuples

use 'prove_sorry'

for code equations that coincide with ctr equations, make sure the usr's input is preserved for both

made 'datatype_new_compat' work with sort constraints

merge