search

equivio / silent-step-spectroscopy

Isabelle formalization of linear-time–branching-time spectroscopy accounting for silent steps
https://equivio.github.io/silent-step-spectroscopy/AFP/LinearTimeBranchingTimeSpectroscopyAccountingForSilentSteps/index.html
Other
0 stars 0 forks source link

115 documentation lemma 3 #134

Closed crmrtz closed 9 months ago

crmrtz commented 9 months ago

Some general remark at the beginning about what strategy formulas are and why they are used to prove correctness would be helpful. Currently, one is immediatly confronted with a rather lengthy isabelle definition without context.

Very true. Lisa is gonna add all comments regarding strategy formulas and comments on Lemma 2 are in a different PR.

betawave commented 9 months ago

Some general remark at the beginning about what strategy formulas are and why they are used to prove correctness would be helpful. Currently, one is immediatly confronted with a rather lengthy isabelle definition without context.

Very true. Lisa is gonna add all comments regarding strategy formulas and comments on Lemma 2 are in a different PR.

Understood. Apart from that, and the minor point about type setting, I'm fine with the way it is.