summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

"bad" set simplifies statements of many theorems

added cterm_lift_inst_rule

Stronger proofs; work for Otway-Rees

Stronger proofs; work for Otway-Rees

These simpsets must not use miniscoping

Corrected associativity: must be to right, as the type dictatess

Removal of (EX x. P) <-> P and (ALL x. P) <-> P
from ex_simps and all_simps. as they are already in quant_simps.

Improved error handling: if there are syntax or type-checking
errors, prints the name of the offending axiom

Modified proof to work with miniscoping

Now uses thin_tac