IFV, prove one assertion

I would write a TCL procedure that takes the assertion name as the parameter ( or the type as you asked for):

proc only_prove { prop_name } {
assertion -delete -cover
assertion -delete -specification
assertion -add $prop_name
prove
}

then you can just do:
only_prove tb.prop1
etc

You can also use this idea to make a new GUI toolbar button.
Take a look at the following article to see how it's done:
http://www.cdnusers.org/Forums/tabid/52/forumid/64/postid/3933/view/topic/Default.aspx

Steve,

I implemented the button as you suggested. This works well in conjunction with a custom button that runs the following tcl code for this button:

only_prove %s

Make sure you click the box for "selection sensitive to selection" and select from the drop down to make this a FormalVerifier script command.

Consider not delelting all assertions in the proc as you will not be able to get results at the end of the run via the assertion -show command. In otherwords, put the commands:

ass -del -all

in the base tcl script and have the proc add the specified assertion and prove. You will then accumulate results in the gui and ass -show tcl command.

JB