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

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

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

Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys

The dtac was discarding information, though apparently no proofs were hurt

Fixed bug in inst_split.

improved big_rec_name lookup;

Updated comments. A bug causes MLWorks to use much
more storage than necessary

Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
goal then it raises exception TRANS. Top-level tactics (blast_tac)
generate warnings and then fail immediately.

Tuned function mk_cntxt_splitthm.
Fixed bug which caused split_tac to fail when
(Const ("splitconst", ...) $ ...) was of function type.

Removed
"(ALL x:f``A. P x) = (ALL x:A. P(f x))",
"(EX x:f``A. P x) = (EX x:A. P(f x))",
again, because they were already there and added
"(UN x:f``A. B x) = (UN a:A. B(f a))"
"(INT x:f``A. B x) = (INT a:A. B(f a))"
instead.

Redesigned the decision procedures for (Abelian) groups and commutative rings.

Added
> "(? x : f `` A. P x) = (? a:A. P(f a))"
> "(! x : f `` A. P x) = (! a:A. P(f a))"