User Details
User Details
- User Since
- Sep 26 2019, 6:21 AM (208 w, 3 d)
Aug 20 2023
Aug 20 2023
sitegen for Fixed_Length_Vector
moved abstract to root.tex
traytel committed rAFPd73b9d89ba85: made proofs more robust.
made proofs more robust
added syntax bundles and disabled syntax by default
new entry Fixed_Length_Vector
Aug 8 2023
Aug 8 2023
traytel committed rISABELLEda437a9f2823: made another two tactics more robust in presence of BNFs nesting live variables….
made another two tactics more robust in presence of BNFs nesting live variables…
traytel committed rISABELLEe72f8009a4f0: made tactic more robust in presence of BNFs nesting live variables (reported by….
made tactic more robust in presence of BNFs nesting live variables (reported by…
Oct 28 2022
Oct 28 2022
traytel committed rISABELLEfc35dc967344: separate out definition of bound to avoid spurious sort hypotheses (by Jan van….
separate out definition of bound to avoid spurious sort hypotheses (by Jan van…
Jun 28 2022
Jun 28 2022
strict bounds for BNFs (by Jan van Brügge)
traytel committed rISABELLE0dd3ac5fdbaa: tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS.
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
strict bounds for BNFs (by Jan van Brügge)
Nov 3 2021
Nov 3 2021
add documentation for pred_mono
Apr 13 2021
Apr 13 2021
updated paper references
Mar 11 2021
Mar 11 2021
another example for lift_bnf for quotients
Mar 9 2021
Mar 9 2021
traytel committed rISABELLE180981b87929: generalized confluence-based subdistributivity theorem for quotients;.
generalized confluence-based subdistributivity theorem for quotients;
Sep 20 2020
Sep 20 2020
traytel committed rAFP21a828811b10: locally deactivated simproc defined_all (following afp/81a8bf702c09).
locally deactivated simproc defined_all (following afp/81a8bf702c09)
traytel committed rAFP5c06d2f30891: replaced ceiling brackets by guillemots (following afp/fb851cb1ca27).
replaced ceiling brackets by guillemots (following afp/fb851cb1ca27)
isabelle update_cartouches -t;
May 31 2020
May 31 2020
simplified Let constructor
Mar 30 2020
Mar 30 2020
avoid nonterminal clash in syntax translation
Mar 15 2020
Mar 15 2020
traytel committed rISABELLE1cf958713cf7: remove Thm.transfer workaround made obsplete by cf2406e654cf.
remove Thm.transfer workaround made obsplete by cf2406e654cf
Feb 29 2020
Feb 29 2020
tuned lift_bnf's user interface for quotients
Feb 24 2020
Feb 24 2020
traytel committed rISABELLEd7ef73df3d15: lift BNF witnesses for quotients (unless better ones are specified by the user).
lift BNF witnesses for quotients (unless better ones are specified by the user)
Feb 20 2020
Feb 20 2020
traytel committed rISABELLE5e25a693c5cf: additional lemmas about alw and suntil (by Michael Foster).
additional lemmas about alw and suntil (by Michael Foster)
Jan 19 2020
Jan 19 2020
traytel committed rISABELLEfce780f9c9c6: new examples of BNF lifting across quotients using a new theory of confluence,.
new examples of BNF lifting across quotients using a new theory of confluence,
Jan 7 2020
Jan 7 2020
traytel committed rISABELLEc71a44893645: eliminated one redundant proof obligation in lift_bnf for quotients.
eliminated one redundant proof obligation in lift_bnf for quotients
Dec 18 2019
Dec 18 2019
made LFP operation more faithful to the implementation