Several places in the tutorial depend, in a fragile way, on the specific ordering of theorems in set.mm, because there's no way to say LOC_BEFORE=statement. You can only say LOC_AFTER=. But in all the tutorial cases, what you really want is to say "put this theorem BEFORE that one".
Could LOC_BEFORE=statement be added so that the tutorial would be more like to work over time?
Several places in the tutorial depend, in a fragile way, on the specific ordering of theorems in set.mm, because there's no way to say LOC_BEFORE=statement. You can only say LOC_AFTER=. But in all the tutorial cases, what you really want is to say "put this theorem BEFORE that one".
Could LOC_BEFORE=statement be added so that the tutorial would be more like to work over time?