converted wt into a set, tuned names

use strip_typeN in bnf_def (instead of repairing strip_type)

removing find_theorems commands that were left in the developments accidently

tuning

tuned code to avoid special case for "fun"

tuned induction tactic

tuned error message

tuning

typeclass formalising bounded subtraction

dropped some unused identifiers

export rel_mono theorem

merged two unfold steps

took out one rotate_tac

killed spurious rotate_tac; use auto instead of blast

moved blast tactic to where it is actually needed

fixed bug in "mk_map" for the "fun" case

correct generalization to 3 or more mutually recursive datatypes

provide more guidance, exploiting our knowledge of the goal

fixed issue with bound variables in prem prems + tuning

use right version of "mk_UnIN"

select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking

tuned code before fixing "mk_induct_discharge_prem_prems_tac"

tuned proofs;

merged

polished the induction

put the flat at the right place (to avoid exceptions)

fixed variable exporting problem

compile

added induct tactic

tuning

renamed "mk_UnN" to "mk_UnIN"

merged two commands