separate out definition of bound to avoid spurious sort hypotheses (by Jan van…

merged

tuned BNF bound

strict bounds for BNFs (by Jan van Brügge)

tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS

strict bounds for BNFs (by Jan van Brügge)

add documentation for pred_mono

updated paper references

another example for lift_bnf for quotients

generalized confluence-based subdistributivity theorem for quotients;

locally deactivated simproc defined_all (following afp/81a8bf702c09)

replaced ceiling brackets by guillemots (following afp/fb851cb1ca27)

isabelle update_cartouches -t;

simplified Let constructor

avoid nonterminal clash in syntax translation

remove Thm.transfer workaround made obsplete by cf2406e654cf

tuned lift_bnf's user interface for quotients

merged

lift BNF witnesses for quotients (unless better ones are specified by the user)

merged

additional lemmas about alw and suntil (by Michael Foster)

new examples of BNF lifting across quotients using a new theory of confluence,

merged

eliminated one redundant proof obligation in lift_bnf for quotients

made LFP operation more faithful to the implementation