| 1997-12-23 | paulson | 1997-12-23 | Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac | file | diff | annotate |
| 1997-12-03 | paulson | 1997-12-03 | Instantiated the one-point-rule quantifier simpprocs for FOL New file fologic.ML holds abstract syntax operations Also, miniscoping provided for intuitionistic logic | file | diff | annotate |