nipkow [Thu, 04 Dec 1997 12:44:37 +0100] rev 4360
pred n -> n-1
nipkow [Thu, 04 Dec 1997 09:05:59 +0100] rev 4359
Simplified proofs.
nipkow [Thu, 04 Dec 1997 09:05:39 +0100] rev 4358
Added thm mult_div_cancel
nipkow [Wed, 03 Dec 1997 17:31:25 +0100] rev 4357
n ~= 0 should become 0 < n
nipkow [Wed, 03 Dec 1997 17:25:43 +0100] rev 4356
Replaced n ~= 0 by 0 < n
wenzelm [Wed, 03 Dec 1997 12:55:04 +0100] rev 4355
pass return code!!
paulson [Wed, 03 Dec 1997 11:42:45 +0100] rev 4354
Fixed the treatment of substitution for equations, restricting occurrences of
variables on the RHS. Improves performance in many cases, though a few old
proofs fail
paulson [Wed, 03 Dec 1997 11:00:24 +0100] rev 4353
updated for latest Blast_tac, which treats equality differently
paulson [Wed, 03 Dec 1997 10:52:17 +0100] rev 4352
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson [Wed, 03 Dec 1997 10:50:02 +0100] rev 4351
Tidying and some comments