equal
deleted
inserted
replaced
37 subsubsection\<open>declarations for tactics\<close> |
37 subsubsection\<open>declarations for tactics\<close> |
38 |
38 |
39 declare analz_subset_parts [THEN subsetD, dest] |
39 declare analz_subset_parts [THEN subsetD, dest] |
40 declare parts_insert2 [simp] |
40 declare parts_insert2 [simp] |
41 declare analz_cut [dest] |
41 declare analz_cut [dest] |
42 declare split_if_asm [split] |
42 declare if_split_asm [split] |
43 declare analz_insertI [intro] |
43 declare analz_insertI [intro] |
44 declare Un_Diff [simp] |
44 declare Un_Diff [simp] |
45 |
45 |
46 subsubsection\<open>extract the agent number of an Agent message\<close> |
46 subsubsection\<open>extract the agent number of an Agent message\<close> |
47 |
47 |