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

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

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

refined 'abbreviation';

made symlink relative

made symlink relative

converted Müller to Mueller to make smlnj 110.58 work

Fixed bug that caused proof of induction rule to fail
for inductive sets with trivial introduction rules
such as "x : S ==> x : S".

remame ASeries to Arithmetic_Series

Fri, 07 Apr 2006 11:17:44 +0200
Added alternative version of thms_of_proof that does not recursively

Added alternative version of thms_of_proof that does not recursively
descend into proofs of (named) theorems.

hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.

filter now accepts axioms as thm, instead of term.

tptp_write_file accepts axioms as thm.