sitegen for Fixed_Length_Vector

moved abstract to root.tex

made proofs more robust

added syntax bundles and disabled syntax by default

new entry Fixed_Length_Vector

made another two tactics more robust in presence of BNFs nesting live variables…

made tactic more robust in presence of BNFs nesting live variables (reported by…

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