| changeset 56059 | 2390391584c2 |
| parent 55142 | 378ae9e46175 |
| child 58305 | 57752a91eec4 |
--- a/src/Doc/Tutorial/Protocol/Message.thy Wed Mar 12 12:18:41 2014 +0100 +++ b/src/Doc/Tutorial/Protocol/Message.thy Wed Mar 12 14:17:13 2014 +0100 @@ -9,7 +9,6 @@ theory Message imports Main begin ML_file "../../antiquote_setup.ML" -setup Antiquote_Setup.setup (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"