Page MenuHomeIsabelle/Phabricator

traytel (Dmitriy Traytel)
User

Projects

User Details

User Since
Sep 26 2019, 6:21 AM (208 w, 3 d)

Recent Activity

Aug 20 2023

traytel committed rAFPa2537884648b: sitegen for Fixed_Length_Vector.
sitegen for Fixed_Length_Vector
Aug 20 2023, 1:10 PM
traytel committed rAFP3e56c4a0b948: moved abstract to root.tex.
moved abstract to root.tex
Aug 20 2023, 1:10 PM
traytel committed rAFPd73b9d89ba85: made proofs more robust.
made proofs more robust
Aug 20 2023, 1:10 PM
traytel committed rAFP231cdb5293e7: added syntax bundles and disabled syntax by default.
added syntax bundles and disabled syntax by default
Aug 20 2023, 1:10 PM
traytel committed rAFP7f4d917a2669: new entry Fixed_Length_Vector.
new entry Fixed_Length_Vector
Aug 20 2023, 1:10 PM

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…
Aug 8 2023, 5:49 PM
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…
Aug 8 2023, 7:26 AM

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…
Oct 28 2022, 12:34 PM

Jun 28 2022

traytel committed rAFP969d123ac0b9: merged.
merged
Jun 28 2022, 10:32 AM
traytel committed rAFP2500a913c1f2: tuned BNF bound.
tuned BNF bound
Jun 28 2022, 10:32 AM
traytel committed rAFP5b2658c54443: strict bounds for BNFs (by Jan van Brügge).
strict bounds for BNFs (by Jan van Brügge)
Jun 28 2022, 10:32 AM
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
Jun 28 2022, 10:31 AM
traytel committed rISABELLE22d1c5f2b9f4: strict bounds for BNFs (by Jan van Brügge).
strict bounds for BNFs (by Jan van Brügge)
Jun 28 2022, 10:31 AM

Nov 3 2021

traytel committed rISABELLE432b3605933d: add documentation for pred_mono.
add documentation for pred_mono
Nov 3 2021, 11:03 AM

Apr 13 2021

traytel committed rAFPbf041f4c01bf: updated paper references.
updated paper references
Apr 13 2021, 9:27 AM

Mar 11 2021

traytel committed rISABELLEbe11fe268b33: another example for lift_bnf for quotients.
another example for lift_bnf for quotients
Mar 11 2021, 10:27 AM

Mar 9 2021

traytel committed rISABELLE180981b87929: generalized confluence-based subdistributivity theorem for quotients;.
generalized confluence-based subdistributivity theorem for quotients;
Mar 9 2021, 6:17 PM

Sep 20 2020

traytel committed rAFP21a828811b10: locally deactivated simproc defined_all (following afp/81a8bf702c09).
locally deactivated simproc defined_all (following afp/81a8bf702c09)
Sep 20 2020, 2:06 PM
traytel committed rAFP5c06d2f30891: replaced ceiling brackets by guillemots (following afp/fb851cb1ca27).
replaced ceiling brackets by guillemots (following afp/fb851cb1ca27)
Sep 20 2020, 2:06 PM
traytel committed rAFPcead889b4653: isabelle update_cartouches -t;.
isabelle update_cartouches -t;
Sep 20 2020, 2:06 PM

May 31 2020

traytel committed rAFPb5440f7e5a01: simplified Let constructor.
simplified Let constructor
May 31 2020, 10:17 PM

Mar 30 2020

traytel committed rAFPbde08698d726: avoid nonterminal clash in syntax translation.
avoid nonterminal clash in syntax translation
Mar 30 2020, 9:02 PM

Mar 15 2020

traytel committed rISABELLE1cf958713cf7: remove Thm.transfer workaround made obsplete by cf2406e654cf.
remove Thm.transfer workaround made obsplete by cf2406e654cf
Mar 15 2020, 1:42 PM

Feb 29 2020

traytel committed rISABELLEcbe0b6b0bed8: tuned lift_bnf's user interface for quotients.
tuned lift_bnf's user interface for quotients
Feb 29 2020, 11:11 AM

Feb 24 2020

traytel committed rISABELLEb94053ca8d77: merged.
merged
Feb 24 2020, 11:18 PM
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 24 2020, 11:18 PM

Feb 20 2020

traytel committed rISABELLEed8d50969995: merged.
merged
Feb 20 2020, 9:14 AM
traytel committed rISABELLE5e25a693c5cf: additional lemmas about alw and suntil (by Michael Foster).
additional lemmas about alw and suntil (by Michael Foster)
Feb 20 2020, 9:14 AM

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 19 2020, 11:15 AM

Jan 7 2020

traytel committed rISABELLE15c6f253b9f3: merged.
merged
Jan 7 2020, 5:13 PM
traytel committed rISABELLEc71a44893645: eliminated one redundant proof obligation in lift_bnf for quotients.
eliminated one redundant proof obligation in lift_bnf for quotients
Jan 7 2020, 5:13 PM

Dec 18 2019

traytel committed rAFP0b9412db8759: made LFP operation more faithful to the implementation.
made LFP operation more faithful to the implementation
Dec 18 2019, 9:01 AM