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

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.

added another function for CNF.

lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.

renamed ASeries to Arithmetic_Series, removed the ^M

modified the perm_compose rule such that it
is applied as simplification rule (as simproc)
in the restricted case where the first
permutation is a swapping coming from a supports
problem
also deleted the perm_compose' rule from the set
of rules that are automatically tried