Skip to content

Make uPred itself independent of BI interface and just prove primitive laws (like in master branch)

Ralf Jung requested to merge ralf/upred into gen_proofmode

The BI interface is then instantiated using these laws. In particular, this shows that the rules we claim to be admissible actually are.

Merge request reports