sitegen for Broadcast_Psi

new entry Broadcast_Psi

sitegen for Approximate_Model_Counting

tuned (removing warnings)

new entry Approximate_Model_Counting

merged

export BNF properties about the cardinal bound (by Jan van Brügge)

sitegen for Sumcheck Protocol

new entry Sumcheck Protocol

made destructor-view tactic more robust (by Jan van Brügge)

merged

made lift_bnf more robust for abstract types with 'phantom' type variables

sitegen for Q0_soundness

new entry Q0_Soundness

adjusted doi capitalization

sitegen for Cardinality_Continuum

new entry Cardinality_Continuum

sitegen for Q0_Metatheory

new entry Q0_Metatheory

updated LaTeX citations

refactored proof

new entry ML_Unification

sitegen

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