--- a/src/ZF/Order.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Order.ML Sat Feb 15 17:52:31 1997 +0100
@@ -11,6 +11,8 @@
open Order;
+val op addss = op unsafe_addss;
+
(** Basic properties of the definitions **)
(*needed?*)
@@ -237,11 +239,10 @@
(*Rewriting with bijections and converse (function inverse)*)
val bij_inverse_ss =
- !simpset setsolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type,
+ !simpset setSolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type,
bij_converse_bij, comp_fun, comp_bij])
addsimps [right_inverse_bij, left_inverse_bij];
-
(** Symmetry and Transitivity Rules **)
(*Reflexivity of similarity*)