# HG changeset patch
# User nipkow
# Date 908804090 -7200
# Node ID 5dc45f44919868d552ac3b5244a4c66d2dc821cd
# Parent  329225a6b6e089b2dc619121ddf38beceef1c202
Addsimps [max_le_iff_conj];
Addsimps [le_min_iff_conj];

diff -r 329225a6b6e0 -r 5dc45f449198 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Mon Oct 19 15:34:26 1998 +0200
+++ b/src/HOL/Ord.ML	Mon Oct 19 15:34:50 1998 +0200
@@ -108,12 +108,15 @@
 by (cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "max_le_iff_conj";
+Addsimps [max_le_iff_conj];
 
 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
 by (Simp_tac 1);
 by (cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "le_min_iff_conj";
+Addsimps [le_min_iff_conj];
+(* AddIffs screws up a blast_tac in MiniML *)
 
 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
 by (Simp_tac 1);