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

match order of generated theorems to user input; improve exhaustiveness criterion to prevent exception

typo

ensure that schematic type variables are fresh in rty

ensure that the raw type of an abstract type cannot be treated as an abstract type recursively

tuned

avoid hard tabs in output -- somewhat ill-defined;

uniform output of tracing via official channel (usually depending on trace flag); warning subject to context visibility;

tuned

merged

more informative error message;

obsolete / unmaintained;

misc tuning and clarification;

more formal ISABELLE_BROWSER_INFO;

tuned comments;

dropped legacy

order and graph for code symbols

special treatment of ==> and == solely as constants