Page MenuHomeIsabelle/Phabricator

traytel (Dmitriy Traytel)
User

Projects

User Details

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

Recent Activity

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