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

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

Now uses thin_tac

Renaming of _rews to _simps

Added thin_tac to signature; previous change was useless