# HG changeset patch
# User paulson
# Date 956135399 -7200
# Node ID 61bc5ed22b621c6ef63f5639eddc52868d7ea56a
# Parent  fa6c4e4182d9a9f33aa80a4a50f95e35af495c01
removal of less_SucI, le_SucI from default simpset

diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOL/Auth/KerberosIV.ML
--- a/src/HOL/Auth/KerberosIV.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOL/Auth/KerberosIV.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -808,7 +808,7 @@
 by analz_sees_tac;
 by (ALLGOALS 
     (asm_simp_tac 
-     (simpset() addsimps ([Says_Kas_message_form, 
+     (simpset() addsimps ([Says_Kas_message_form, less_SucI,
 			   analz_insert_eq, not_parts_not_analz, 
 			   analz_insert_freshK1] @ pushes))));
 (*Fake*) 
@@ -868,9 +868,11 @@
 by (rotate_tac ~1 11);
 by (ALLGOALS 
     (asm_full_simp_tac 
-     (simpset() addsimps ([Says_Kas_message_form, Says_Tgs_message_form,
-			   analz_insert_eq, not_parts_not_analz, 
-			   analz_insert_freshK1, analz_insert_freshK2] @ pushes))));
+     (simpset() addsimps [less_SucI, 
+			  Says_Kas_message_form, Says_Tgs_message_form,
+			  analz_insert_eq, not_parts_not_analz, 
+			  analz_insert_freshK1, analz_insert_freshK2] 
+			 @ pushes)));
 (*Fake*) 
 by (spy_analz_tac 1);
 (*K2*)
diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -239,8 +239,9 @@
 by (etac kerberos_ban.induct 1);
 by analz_spies_tac;
 by (ALLGOALS
-    (asm_simp_tac (simpset() addsimps [analz_insert_eq, analz_insert_freshK]
-				      @ pushes)));
+    (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq, 
+				       analz_insert_freshK]
+		                      @ pushes)));
 (*Oops*)
 by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
 (*Kb2*)
diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOL/Finite.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -457,10 +457,10 @@
 by (Clarify_tac 1);
 by (case_tac "x:B" 1);
  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
- by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
-by (fast_tac (claset() addss
-	      (simpset() addsimps [subset_insert_iff, finite_subset]
-			 delsimps [insert_subset])) 1);
+ by (asm_full_simp_tac (simpset() addsimps [le_SucI, subset_insert_iff]) 2);
+by (force_tac (claset(),
+	       simpset() addsimps [subset_insert_iff, finite_subset]
+			 delsimps [insert_subset]) 1);
 qed_spec_mp "card_mono";
 
 
@@ -514,7 +514,7 @@
 by (eres_inst_tac [("P","?a<?b")] notE 1);
 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1);
 by (case_tac "A=F" 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_SucI])));
 qed_spec_mp "psubset_card" ;
 
 Goal "[| A <= B; card B <= card A; finite B |] ==> A = B";
@@ -533,7 +533,7 @@
 Goal "finite A ==> card (f `` A) <= card A";
 by (etac finite_induct 1);
 by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [finite_imageI,card_insert_if]) 1);
+by (asm_simp_tac (simpset() addsimps [le_SucI,finite_imageI,card_insert_if]) 1);
 qed "card_image_le";
 
 Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -4,7 +4,7 @@
     Copyright   1998 TUM
 *)
 
-Addsimps [in_set_butlast_appendI];
+Addsimps [in_set_butlast_appendI, less_SucI];
 AddIs    [in_set_butlast_appendI];
 Addsimps [image_eqI];
 
diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOL/List.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -560,6 +560,7 @@
 Goal "length (filter P xs) <= length xs";
 by (induct_tac "xs" 1);
 by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [le_SucI]) 1);
 qed "length_filter";
 Addsimps[length_filter];
 
diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOL/NatDef.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -140,7 +140,6 @@
 
 (* i<j ==> i<Suc(j) *)
 bind_thm("less_SucI", lessI RSN (2, less_trans));
-Addsimps [less_SucI];
 
 Goal "0 < Suc(n)";
 by (nat_ind_tac "n" 1);
@@ -381,7 +380,6 @@
 Goalw [le_def] "m <= n ==> m <= Suc n";
 by (blast_tac (claset() addDs [Suc_lessD]) 1);
 qed "le_SucI";
-Addsimps[le_SucI];
 
 (*bind_thm ("le_Suc", not_Suc_n_less_n RS leI);*)
 
diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOLCF/IOA/NTP/Impl.ML
--- a/src/HOLCF/IOA/NTP/Impl.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -7,7 +7,7 @@
 *)
 
 
-Addsimps [Let_def];
+Addsimps [Let_def, le_SucI];
 
 
 open Abschannel Impl;
diff -r fa6c4e4182d9 -r 61bc5ed22b62 src/HOLCF/IOA/Storage/Correctness.ML
--- a/src/HOLCF/IOA/Storage/Correctness.ML	Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOLCF/IOA/Storage/Correctness.ML	Wed Apr 19 11:09:59 2000 +0200
@@ -42,7 +42,7 @@
       Spec.ioa_def,Spec.trans_def,trans_of_def])1);
 (* LOC *)
 by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [less_SucI]) 1);
 by (rtac transition_is_ex 1);
 by (simp_tac (simpset() addsimps [
       Spec.ioa_def,Spec.trans_def,trans_of_def])1);