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

Now uses DB-ROOT.ML, which is separate from ROOT.ML

Dedicated root file for making the Auth database

Beefed-up auto-tactic: now repeatedly simplifies if needed

"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.