Reordered rules in analz_image_freshK_ss to improve clarity
authorpaulson
Tue Jul 01 17:36:42 1997 +0200 (1997-07-01)
changeset 34792aacd6f10654
parent 3478 770939fecbb3
child 3480 d59bbf053258
Reordered rules in analz_image_freshK_ss to improve clarity
src/HOL/Auth/Shared.ML
     1.1 --- a/src/HOL/Auth/Shared.ML	Tue Jul 01 17:35:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/Shared.ML	Tue Jul 01 17:36:42 1997 +0200
     1.3 @@ -365,11 +365,10 @@
     1.4    erase occurrences of forwarded message components (X).*)
     1.5  val analz_image_freshK_ss = 
     1.6       !simpset delsimps [image_insert, image_Un]
     1.7 -              addsimps ([analz_insert_eq, Key_not_used, 
     1.8 -			 impOfSubs (Un_upper2 RS analz_mono),
     1.9 -                         image_insert RS sym, image_Un RS sym,
    1.10 +              addsimps ([image_insert RS sym, image_Un RS sym,
    1.11 +                         analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
    1.12                           insert_Key_singleton, subset_Compl_range,
    1.13 -                         insert_Key_image, Un_assoc RS sym]
    1.14 +                         Key_not_used, insert_Key_image, Un_assoc RS sym]
    1.15                          @disj_comms)
    1.16                setloop split_tac [expand_if];
    1.17