paulson [Thu, 10 Apr 1997 10:55:37 +0200] rev 2929
Changed some fast_tac to blast_tac
nipkow [Thu, 10 Apr 1997 09:08:05 +0200] rev 2928
Added trace output and replaced fast_tac set_cs by Fast_tac.
oheimb [Wed, 09 Apr 1997 15:56:53 +0200] rev 2927
replaced 'addwrapper' and 'addWrapper' by correct 'compwrapper' and 'compWrapper'
nipkow [Wed, 09 Apr 1997 15:26:32 +0200] rev 2926
Thorough update.
paulson [Wed, 09 Apr 1997 12:37:44 +0200] rev 2925
Using Blast_tac
paulson [Wed, 09 Apr 1997 12:36:52 +0200] rev 2924
Control over excessive branching by applying a log2 penalty
Incorporation of debugging features
Allows backtracking over haz rules if alternatives exist
Subsitution for equality may more a rule from the haz to the safe part
paulson [Wed, 09 Apr 1997 12:34:28 +0200] rev 2923
Explicit depth bounds seem necessary
paulson [Wed, 09 Apr 1997 12:32:04 +0200] rev 2922
Using Blast_tac
paulson [Wed, 09 Apr 1997 12:31:11 +0200] rev 2921
Dependency on Provers/nat_transitive
nipkow [Tue, 08 Apr 1997 12:03:59 +0200] rev 2920
Couldn't solve n < n+1 because of missing -1