src/HOL/Quotient_Examples/Quotient_Message.thy
changeset 40468 d4aac200199e
parent 37594 32ad67684ee7
child 40823 37b25a87d7ef
     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 09 14:02:13 2010 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 09 14:02:14 2010 +0100
     1.3 @@ -179,11 +179,11 @@
     1.4  
     1.5  lemma [quot_respect]:
     1.6    shows "(op \<sim> ===> op =) freenonces freenonces"
     1.7 -  by (simp add: msgrel_imp_eq_freenonces)
     1.8 +  by (auto simp add: msgrel_imp_eq_freenonces)
     1.9  
    1.10  lemma [quot_respect]:
    1.11    shows "(op = ===> op \<sim>) NONCE NONCE"
    1.12 -  by (simp add: NONCE)
    1.13 +  by (auto simp add: NONCE)
    1.14  
    1.15  lemma nonces_Nonce [simp]:
    1.16    shows "nonces (Nonce N) = {N}"
    1.17 @@ -191,7 +191,7 @@
    1.18  
    1.19  lemma [quot_respect]:
    1.20    shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
    1.21 -  by (simp add: MPAIR)
    1.22 +  by (auto simp add: MPAIR)
    1.23  
    1.24  lemma nonces_MPair [simp]:
    1.25    shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
    1.26 @@ -214,7 +214,7 @@
    1.27  
    1.28  lemma [quot_respect]:
    1.29    shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
    1.30 -  by (simp add: msgrel_imp_eqv_freeleft)
    1.31 +  by (auto simp add: msgrel_imp_eqv_freeleft)
    1.32  
    1.33  lemma left_Nonce [simp]:
    1.34    shows "left (Nonce N) = Nonce N"
    1.35 @@ -243,7 +243,7 @@
    1.36  
    1.37  lemma [quot_respect]:
    1.38    shows "(op \<sim> ===> op \<sim>) freeright freeright"
    1.39 -  by (simp add: msgrel_imp_eqv_freeright)
    1.40 +  by (auto simp add: msgrel_imp_eqv_freeright)
    1.41  
    1.42  lemma right_Nonce [simp]:
    1.43    shows "right (Nonce N) = Nonce N"