From 3c36b589a01bce19063872544bca132f3daf947d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 24 Jun 2016 17:15:59 -0400 Subject: folkwisdom: remove redundant idtac --- folkwisdom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'folkwisdom.md') diff --git a/folkwisdom.md b/folkwisdom.md index d87174115..c6190a460 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -211,7 +211,7 @@ buffer in `proofgeneral`). A useful heuristic for reading that log is to look for the first place where the resolution backtracks and then read backwards from there. 5. To perform multiple rewrites at once, make rewrite hint database and call -`idtac; (rewrite_strat topdown hints dbname).` where `topdown` can be replaced +`(rewrite_strat topdown hints dbname).` where `topdown` can be replaced with `bottomup` for different behavior. This does not seem to unfold definitions, so it may be a reasonable alternative to using `Local Opaque` to protect definitions from `setoid_rewrite`. -- cgit v1.2.3