Reordered rules in analz_image_freshK_ss to improve clarity
authorpaulson
Tue, 01 Jul 1997 17:36:42 +0200
changeset 3479 2aacd6f10654
parent 3478 770939fecbb3
child 3480 d59bbf053258
Reordered rules in analz_image_freshK_ss to improve clarity
src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Tue Jul 01 17:35:09 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Tue Jul 01 17:36:42 1997 +0200
@@ -365,11 +365,10 @@
   erase occurrences of forwarded message components (X).*)
 val analz_image_freshK_ss = 
      !simpset delsimps [image_insert, image_Un]
-              addsimps ([analz_insert_eq, Key_not_used, 
-			 impOfSubs (Un_upper2 RS analz_mono),
-                         image_insert RS sym, image_Un RS sym,
+              addsimps ([image_insert RS sym, image_Un RS sym,
+                         analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
                          insert_Key_singleton, subset_Compl_range,
-                         insert_Key_image, Un_assoc RS sym]
+                         Key_not_used, insert_Key_image, Un_assoc RS sym]
                         @disj_comms)
               setloop split_tac [expand_if];