Commit 7682c6fc authored by Michael Sammler's avatar Michael Sammler

add hooks to spinlock example

parent 341fdd3e
......@@ -24,7 +24,7 @@ Section type.
repeat liRStep; liShow.
liInst Hevar γ.
repeat liRStep; liShow.
Unshelve. all: prepare_sideconditions; solve_goal.
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
Qed.
End type.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment