Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-08 13:31:36 -0700 (Wed, 08 May 2002)
Revision: 3609
Log message:
- Changed the top_bookmark implementation to make it more explicit that
it's always the same bookmark.
- The apply_rewrite now expects a bookmark as its input (Brian, is that OK?)
There are 3 ways of getting a bookmark:
1) Use ("Theory", "rule") for a bookmark pointing right *before*
a rule (rewrite) is defined.
2) Use Mp_resource.theory_bookmark "Theory" for a bookmark
pointing at the end of the theory
3) Use let _ = Mp_resource.bookmark "foo" in a theory to create a bookmark and
then refer to it as ("Theory", "foo")