User Details
User Details
- User Since
- Sep 26 2019, 6:21 AM (174 w, 1 d)
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