--- a/src/HOL/AxClasses/Lattice/Order.ML Mon Apr 27 16:45:11 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/Order.ML Mon Apr 27 16:45:27 1998 +0200
@@ -115,7 +115,7 @@
(** limits in linear orders **)
goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)";
- by (stac expand_if 1);
+ by (stac split_if 1);
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
(*case "x [= y"*)
by (rtac le_refl 1);
@@ -131,7 +131,7 @@
qed "min_is_inf";
goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)";
- by (stac expand_if 1);
+ by (stac split_if 1);
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
(*case "x [= y"*)
by (assume_tac 1);