mn200

Protecting Assumptions

Certain assumption types are naturally thought of being at least a bit protected. To be protected is to be somewhat immune to destructive changes.

“Destructive Changes”

Changes in Place: at the bottom level, there are relatively few facilities for changing assumptions in place other than with RULE_ASSUM_TAC. Of course, tactics can just access assumption lists directly, but most don't.

mn200

Keybase proof

I hereby claim:

• I am mn200 on github.
• I am michaeln (https://keybase.io/michaeln) on keybase.
• I have a public key whose fingerprint is 1638 8636 37E5 313B 3BBF 5075 6286 43A7 A3DD 1D91

To claim this, I am signing this object:

mn200

*.html

mn200

Installing Z3 version 4.0

1. Download and unpack tar-ball from MSR download site.

2. Run the z3 executable in z3/bin. Simple!