# HG changeset patch
# User oheimb
# Date 936634720 -7200
# Node ID 45905028bb1d0ddcbd9beb72692131be701f7ef1
# Parent  e6f74eebfab31426ec2eada1c44e27c9de1ead1a
added theorems le_maxI1 and le_maxI2, also in claset

diff -r e6f74eebfab3 -r 45905028bb1d src/HOL/Auth/KerberosIV.ML
--- a/src/HOL/Auth/KerberosIV.ML	Mon Sep 06 18:18:30 1999 +0200
+++ b/src/HOL/Auth/KerberosIV.ML	Mon Sep 06 18:18:40 1999 +0200
@@ -713,14 +713,16 @@
                  RS parts.Snd RS parts.Snd RS parts.Snd] 2);
 by (Asm_full_simp_tac 2);
 by (blast_tac (claset() addSDs [ServKey_not_KeyCryptKey] 
+			delrules [le_maxI1, le_maxI2]
                         addDs [impOfSubs analz_mono]) 2);
-(*Level 28: Oops 1*)
+(*Level 27: Oops 1*)
 by (dres_inst_tac [("x","SK")] spec 1);
 by (dres_inst_tac [("x","insert AuthKey KK")] spec 1);
 by (case_tac "KeyCryptKey AuthKey SK evsO1" 1);
 by (ALLGOALS Asm_full_simp_tac);
 by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1);
-by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
+by (blast_tac (claset() delrules [le_maxI1, le_maxI2] 
+			addDs [impOfSubs analz_mono]) 1);
 qed_spec_mp "Key_analz_image_Key";
 
 
diff -r e6f74eebfab3 -r 45905028bb1d src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Mon Sep 06 18:18:30 1999 +0200
+++ b/src/HOL/Ord.ML	Mon Sep 06 18:18:40 1999 +0200
@@ -154,6 +154,12 @@
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "le_max_iff_disj";
 
+qed_goal "le_maxI1" Ord.thy "(x::'a::linorder) <= max x y" 
+	(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI1) 1]);
+qed_goal "le_maxI2" Ord.thy "(y::'a::linorder) <= max x y" 
+	(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI2) 1]);
+AddSIs[le_maxI1, le_maxI2];
+
 Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
 by (simp_tac (simpset() addsimps [order_le_less]) 1);
 by (cut_facts_tac [linorder_less_linear] 1);