IOA/example/Impl.ML

--- a/IOA/example/Impl.ML	Wed Mar 01 17:32:10 1995 +0100
+++ b/IOA/example/Impl.ML	Wed Mar 01 17:37:09 1995 +0100
@@ -105,10 +105,9 @@
 by (hyp_subst_tac 1);
 
 by (rtac (pred_suc RS mp RS sym RS iffD2) 1);
-by (dmatch_tac [less_leq_less RS mp] 1);
+by (dtac less_le_trans 1);
 by (cut_facts_tac [rewrite_rule[Packet.hdr_def]
-                    eq_packet_imp_eq_hdr RS countm_props] 1);;
-by (dtac mp 1);
+		   eq_packet_imp_eq_hdr RS countm_props] 1);;
 by (assume_tac 1);
 by (assume_tac 1);
 
@@ -163,7 +162,7 @@
                                 (inv1 RS invariantE) RS conjunct1] 1);
   by (asm_full_simp_tac (impl_ss addsimps [Impl.inv2_def] 
                                  addsimps transitions) 1);
-  by (fast_tac (HOL_cs addDs [plus_leD1,leD]) 1);
+  by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
 
   (* 3 *)
   by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
@@ -171,7 +170,7 @@
   by (asm_full_simp_tac (impl_ss addsimps 
                          (Impl.inv2_def::transitions)) 1);
   by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
-  by (fast_tac (HOL_cs addDs [plus_leD1,leD]) 1);
+  by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
 
   (* 2 *)
   by (asm_full_simp_tac (impl_ss addsimps 
@@ -376,7 +375,7 @@
                                (inv3 RS invariantE)] 1);
   by (asm_full_simp_tac list_ss 1);
   by (eres_inst_tac [("x","m")] allE 1);
-  by (dtac (less_leq_less RS mp RS mp) 1);
+  by (dtac less_le_trans 1);
   by (dtac (left_add_leq RS mp) 1);
   by (asm_full_simp_tac list_ss 1);
   by (asm_full_simp_tac arith_ss 1);