# HG changeset patch
# User lcp
# Date 784546311 -3600
# Node ID 74ee8b9ff9a7c97a014c6c0bd64a745e64b24f36
# Parent  31f50c1778effe0d4b720f8bade700cb04ca441d
argument swaps in HOL

diff -r 31f50c1778ef -r 74ee8b9ff9a7 doc-src/ERRATA.txt
--- a/doc-src/ERRATA.txt	Thu Nov 10 11:36:40 1994 +0100
+++ b/doc-src/ERRATA.txt	Fri Nov 11 10:31:51 1994 +0100
@@ -81,6 +81,18 @@
 	PowI     A<=B ==> A: Pow(B)
 	PowD     A: Pow(B) ==> A<=B
 
+page 251: split now has type [['a,'b] => 'c, 'a * 'b] => 'c
+Definition modified accordingly
+
+page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c
+Definition and rules modified accordingly
+
+page 254: nat_case now has type ['a, nat=>'a, nat] =>'a
+Definition modified accordingly
+
+page 256,258: list_case now takes the list as its last argument, not the
+first.
+
 page 259: HOL theory files may now include datatype declarations, primitive
 recursive function definitions, and (co)inductive definitions.  (These new
 sections are available separately as the file ml/HOL-extensions.dvi.gz,