wenzelm [Fri, 31 Mar 1995 15:09:21 +0200] rev 237
replaced 'arities' by 'instance';
lcp [Thu, 30 Mar 1995 13:39:36 +0200] rev 236
Defined addss to perform simplification in a claset.
Precedence of addcongs is now 4 (to match that of other simplifier infixes)
clasohm [Tue, 28 Mar 1995 12:48:46 +0200] rev 235
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
apfst from Pure/library.ML
nipkow [Mon, 27 Mar 1995 18:30:04 +0200] rev 234
Added recursion equations for foldl to list_ss.
nipkow [Fri, 17 Mar 1995 15:48:55 +0100] rev 233
Added a few thms to nat_ss and list_ss
lcp [Wed, 15 Mar 1995 10:44:26 +0100] rev 232
Now calls exit_use instead of use, for prompt failure if errors are detected.
nipkow [Tue, 14 Mar 1995 09:43:12 +0100] rev 231
Removed some type constraints
nipkow [Tue, 14 Mar 1995 09:42:49 +0100] rev 230
added "exit 1"
nipkow [Mon, 13 Mar 1995 09:41:20 +0100] rev 229
Removed unecessary type constraint because instantiations do not freeze type
vars any more.
nipkow [Wed, 08 Mar 1995 17:22:28 +0100] rev 228
Added dependencies on ../Provers/hypsubst.ML and removed those on
../Provers/ind.ML